В Haskell две функции кажутся одинаковыми, но разными - PullRequest
Новая
       32

В Haskell две функции кажутся одинаковыми, но разными

4 голосов
/ 12 мая 2019

Я пытаюсь реализовать логическое значение без Prelude в Haskell.

Когда вычисляется выражение beq true true "TRUE" "FALSE", ничего страшного. Но когда я пытаюсь оценить beq' true true "TRUE" "FALSE", происходит сбой из-за разницы между ожидаемым типом и фактическим типом.

Это код. 

import qualified Prelude as P

i = \x -> x
k = \x y -> x
ki = k i

true = k
false = ki

not = \p -> p false true
beq = \p q -> p (q true false) (q false true)
beq' = \p q -> p q (not q)

Итак, я проверил предполагаемые типы тезисов. 

*Main> :type beq
beq
  :: (t1 -> t1 -> t2)
     -> ((p1 -> p1 -> p1) -> (p2 -> p2 -> p2) -> t1) -> t2

*Main> :type beq'
beq'
  :: (((p1 -> p2 -> p2) -> (p3 -> p4 -> p3) -> t1) -> t1 -> t2)
     -> ((p1 -> p2 -> p2) -> (p3 -> p4 -> p3) -> t1) -> t2

И это не было равным.

Вот вопросы.

  1. Я думал, что у него такая же сигнатура типа, потому что beq и beq', по-видимому, дают тот же результат, когда он складывается и подставляется. Как есть много способов реализовать одну функцию. Но это не так. Есть ли в Haskell какие-то секретные правила и синтаксис?

  2. Если я хочу написать beq с функцией not, как я могу заставить ее работать?

1 Ответ

8 голосов
/ 12 мая 2019

Как исправить кодировку

Церковные кодировки очень хорошо работают в нетипизированном исчислении.

При добавлении типов все усложняется.Например, для простых типов кодировки теряются.С полиморфизмом они могут быть восстановлены, если поддерживаются более высокие ранги.Обратите внимание, что вывод типов не может хорошо работать с более старшими типами, поэтому необходима некоторая явная аннотация типа.

Например, ваш not должен быть записан как: 

{-# LANGUAGE RankNTypes #-}
type ChBool = forall a. a -> a -> a

not :: ChBool -> ChBool
not f x y = f y x

Этоважно, чтобы логические значения моделировались как полиморфные функции, поскольку в противном случае они могут использоваться только для одного типа, что приводит к сбою многих примеров.Например, рассмотрим 

foo :: Bool -> (Int, String)
foo b = (b 3 2, b "aa" "bb")

Здесь b необходимо использовать дважды, один раз на Int с и один раз на String с.Если Bool не является полиморфным, это потерпит неудачу.

Почему бета-редукция меняет выводимый тип

Кроме того, вы, похоже, уверены, что вы можете бета-сокращать выражения Хаскелла и выводимый типдо и после сокращения должно быть одинаковым.В общем, это не так, как вы обнаружили в своих экспериментах.Чтобы понять почему, вот простой пример: 

id1 x = x

Предполагаемый тип здесь, очевидно, id1 :: forall a. a -> a.Вместо этого рассмотрим этот вариант: 

id2 x = (\ _ -> x) e

Обратите внимание, что id2 beta-уменьшает до id1, независимо от того, e может быть .Тщательно выбирая e, мы можем ограничить тип x.Например, давайте выберем e = x "hello"

id2 x = (\ _ -> x) (x "hello")

Теперь выводимый тип - id2 :: forall b. (String -> b) -> String -> b, поскольку x может быть только String -принимающей функцией.Неважно, что e не будет оцениваться, алгоритм вывода типов в любом случае сделает это типизированным.Это делает предполагаемый тип id2 отличным от id1.

...