Co to COMBINATOR zrobić: s (sk)

teraz rozumiem podpis typu z s (s k):Co to COMBINATOR zrobić: s (sk)

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

I mogę stworzyć przykłady, które działają bez błędów w narzędziu Haskell WinGHCi:

przykładu:

s (s k) (\g -> 2) (\x -> 3)

powraca 2.

Przykład:

s (s k) (\g -> g 3) successor

powraca 4.

gdzie successor jest zdefiniowany jako tak:

successor = (\x -> x + 1)

Niemniej jednak, nadal nie mają intuicyjne wyczucie za co s (s k) robi.

Kombinator s (s k) ma dowolne dwie funkcje: f i g. Co robi s (s k) z f i g? Czy podałbyś duże zdjęcie na co proszę s (s k)?

Źródło

2012-03-12 Roger Costello

Brak definicji dla 'S (S K)'. Czy to samo 's' i' k' w http://stackoverflow.com/questions/9592191/the-type-signature-of-a-combinator-does-not-match-the-type-signature-of- its-equi? –

Btw, co jest intuicyjne? Czy uważasz, że http://en.wikipedia.org/wiki/Ouroboros jest intuicyjny? Czy możesz sobie wyobrazić, że wąż je i znika? Lub robot, który sam się buduje? Potrzebujesz lepszego wyczucia czegoś działającego na siebie. –

Dobrze, spójrzmy, co oznacza S (S K). Mam zamiar wykorzystać te definicje:

S = \x y z -> x z (y z) 
K = \x y -> x 

S (S K) = (\x y z -> x z (y z)) ((\x y z -> x z (y z)) (\a b -> a)) -- rename bound variables in K 
     = (\x y z -> x z (y z)) (\y z -> (\a b -> a) z (y z)) -- apply S to K 
     = (\x y z -> x z (y z)) (\y z -> (\b -> z) (y z)) -- apply K to z 
     = (\x y z -> x z (y z)) (\y z -> z) -- apply (\_ -> z) to (y z) 
     = (\x y z -> x z (y z)) (\a b -> b) -- rename bound variables 
     = (\y z -> (\a b -> b) z (y z)) -- apply S to (\a b -> b) 
     = (\y z -> (\b -> b) (y z)) -- apply (\a b -> b) to z 
     = (\y z -> y z) -- apply id to (y z)

Jak widać, to tylko ($) bardziej konkretnego typu.

Źródło

2012-03-12 10:08:01 Vitus

Innym sposobem zobaczenia tego: typem jest '((t1 -> t2) -> t1) -> (t1 -> t2) -> t1'. Dodając nawiasy, otrzymujemy '((t1 -> t2) -> t1) -> ((t1 -> t2) -> t1)'. Pozwalając typowi "α" oznaczać "(t1 -> t2) -> t1", jest to po prostu "α -> α", a więc, przez parametryczność, 's (sk)' jest funkcją identyczności z bardziej szczegółową rodzaj. (I oczywiście '($) :: (a -> b) -> a -> b' jest * także * tylko funkcją identyfikacji o bardziej szczegółowym typie.) –

Rzeczywiście, jeśli η-zredukujemy' \ y -> \ z -> yz', otrzymujemy '\ y -> y'. – Vitus

W kombinatorach S K y z = K z (y z) = z. Następnie S (SK) yz = SKz (yz) = K (yz) (z (yz)) = yz. – rickythesk8r

Odpowiedz

Powiązane problemy