Che cosa significa questo combinatore do: s (sk)

ora capisco la firma tipo di s (s k):Che cosa significa questo combinatore do: s (sk)

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

e posso creare esempi che funzionano senza errori nello strumento Haskell WinGHCi:

Esempio:

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

rendimenti 2.

Esempio:

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

rendimenti 4.

dove successor è definito come così:

successor = (\x -> x + 1)

Ciò nonostante, io ancora non ho una sensazione intuitiva per quello s (s k) fa.

Il combinatore s (s k) accetta due funzioni f e g. Cosa fa s (s k) con f e g? Mi daresti l'immagine grande su cosa s (s k) soddisfa?

fonte

2012-03-12 Roger Costello

Manca la definizione per 'S (S K)'. È lo stesso 's' e' k' in http://stackoverflow.com/questions/9592191/the-type-signature-of-a-combinator-does-not-match-the-type-signature-of- suo-equi? –

Btw, cos'è intuitivo? Hai trovato http://en.wikipedia.org/wiki/Ouroboros intuitivo? Riesci a immaginare un serpente che si mangia e svanisce? O un robot che si costruisce da solo? Hai bisogno di un senso migliore su qualcosa che agisce su se stesso. –

OK, diamo un'occhiata a ciò che significa S (S K). Ho intenzione di usare queste definizioni:

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)

Come si può vedere, è solo ($) con il tipo più specifico.

fonte

2012-03-12 10:08:01 Vitus

Un altro modo per vedere questo: il tipo è '((t1 -> t2) -> t1) -> (t1 -> t2) -> t1'. Aggiungendo parentesi, otteniamo '((t1 -> t2) -> t1) -> ((t1 -> t2) -> t1)'. Lasciando il tipo 'α' sta per' (t1 -> t2) -> t1', questo è solo 'α -> α', e quindi, per parametrricità,' s (sk) 'è la funzione di identità con uno specifico genere. (E ovviamente, '($) :: (a -> b) -> a -> b' è * anche * solo la funzione di identità con un tipo più specifico.) –

Infatti, se riduciamo η' \ y -> \ z -> yz', otteniamo '\ y -> y'. – Vitus

In combinatori, S K y z = K z (y z) = z. Quindi S (S K) y z = S K z (y z) = K (y z) (z (y z)) = y z. – rickythesk8r

Che cosa significa questo combinatore do: s (sk)

risposta

Problemi correlati