deniok

Есть у нас в хозяйстве Curry-Howard isomorphism. Написал

(.) :: (a -> b) -> (b -> c) -> (a -> c)
(.) f g x = f (g x)

доказал теорему логики.

А ещё у нас в хозяйстве есть много чего. Конструкторы данных там, классы типов. И как только у нас возникает тип (x y), где x и/или y под forall, я начинаю терять связь с логикой :(

Что значат типы конструкторов данных с точки зрения логики?

data List a where
              Nil  :: List a
              Cons :: a -> List a -> List a

Доказательств-то (реализации) нет.

С другой стороны есть

build :: forall a . (forall b . b -> (a -> b -> b) -> b) -> List a
build g = g Cons Nil

То есть вроде того, что для каждого a список List a эквивалентен функции с типом
forall b . b -> (a -> b -> b) -> b
Если подставлять это дело вместо List a во все функции, которые имеют в типе List a, то будут выходить теоремы логики?

instance Functor List where
   fmap f Nil         = Nil
   fmap f (Cons x xs) = Cons (f x) (fmap f xs)

То есть тип

fmap :: forall a b. (a -> b) -> List a -> List b

доказывает теорему

forall a b. (a -> b) -> (forall c . c -> (a -> c -> c) -> c)-> (forall d . d -> (b ->d -> d) -> d)
?