Как набрать простейший термин лямбда-исчисление (S K K)

Question

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

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

Оскорбительный термин явно (СКК)

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

Я думаю, что проблема возникает из-за отсутствия полиморфизма, потому что, когда я проверяю тип, этот код haskell работает нормально:

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

но если я специализируюсь на типе:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x y z = x z (y z)
test = s k k -- doesn't type check 

Просто для справки, моя система типов проста:

data Type = T | TArr Type Type

полный источник

Answer 1

Я украду идеи из моего предыдущего ответа, чтобы показать, как задать свой вопрос. Но сначала я собираюсь немного переформулировать ваш вопрос.

В Хаскеле мы имеем

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: a -> b -> a

и вопрос, который мы хотим задать, это "Как эти типы выглядят после проверки типов s k k?". Более того, если мы переписываем их с различными переменными объединения,

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: d -> e -> d
k :: f -> g -> f
s k k :: h

тогда вопрос становится объединяющим: мы пытаемся унифицировать тип s с типом, в котором он используется - а именно (d -> e -> d) -> (f -> g -> f) -> h, Теперь, когда у нас есть вопрос об объединении, мы можем задать его в формате, указанном в моем другом ответе:

> :{
| :t undefined
| ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
|    ~ ((d -> e -> d) -> (f -> g -> f) -> h)
| => (a, b, c, d, e, f, g, h)
| :}
undefined
::   ((a -> b -> c) -> (a -> b) -> (a -> c))
   ~ ((d -> e -> d) -> (f -> g -> f) -> h)
=> (a, b, c, d, e, f, g, h)
  :: (f, g -> f, f, f, g -> f, f, g, f -> f)

И теперь мы можем понять, почему ваша версия не работает: в вашей версии вы создали все полиморфные переменные для базового типа T; но с тех пор b ~ g -> f, e ~ g -> f, а также h ~ f -> f явно типы стрел, которые, безусловно, не сработают! Тем не менее, любой выбор для f а также g будет работать, если мы уважаем замену выше; в частности, если мы выберем f ~ T а также g ~ Tтогда мы имеем

s :: (T -> (T -> T) -> T) -> (T -> (T -> T)) -> (T -> T)
k1 :: T -> (T -> T) -> T
k2 :: T -> T -> T
s k1 k2 :: T -> T