Что это комбинатор сделать: s (ск)

теперь я понимаю, тип подписи s (s k):Что это комбинатор сделать: s (ск)

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

И я могу создать примеры, которые работают без ошибок в инструменте Haskell WinGHCi:

Пример:

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

возвращается 2.

Пример:

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

возвращается 4.

где successor определяется как так:

successor = (\x -> x + 1)

Тем не менее, я до сих пор не имеют интуитивное ощущение для того, что s (s k) делает.

Комбинатор s (s k) выполняет любые две функции: f и g. Что делает s (s k) делать с f и g? Не могли бы вы дать мне большую картинку на что s (s k) не нравится?

источник

2012-03-12 Roger Costello

Отсутствует защита на 'S (S K)'. Является ли это одним и тем же '' и 'k' в http://stackoverflow.com/questions/9592191/the-type-signature-of-a-combinator-does-not-match-the-type-signature-of- его-equi? –

Btw, что интуитивно? Вы нашли http://en.wikipedia.org/wiki/Ouroboros интуитивно понятным? Можете ли вы представить себе, что змея ест себя и исчезает? Или робот, который строит себя от себя? Вам нужно лучше понять что-то, действующее на себя. –

Хорошо, давайте посмотрим, что означает S (S K). Я собираюсь использовать эти определения:

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)

Как вы можете видеть, это просто ($) с более конкретным типом.

источник

2012-03-12 10:08:01 Vitus

Другой способ увидеть это: тип '((t1 -> t2) -> t1) -> (t1 -> t2) -> t1'. Добавляя круглые скобки, получаем '((t1 -> t2) -> t1) -> ((t1 -> t2) -> t1)'. Пусть тип 'α' обозначает' (t1 -> t2) -> t1', это просто 'α -> α', и поэтому, по параметричности,' s (sk) '- это идентификационная функция с более конкретным тип. (И, конечно, '($) :: (a -> b) -> a -> b' * также * - это только тождественная функция с более конкретным типом.) –

Действительно, если мы п-уменьшим' \ y -> \ z -> yz', получаем '\ y -> y'. – Vitus

В комбинаторах S K y z = K z (y z) = z. Тогда S (S K) y z = S K z (y z) = K (y z) (z (y z)) = y z. – rickythesk8r

ответ

Смежные вопросы