Кодировка церкви для зависимых типов: от Coq до Haskell - PullRequest
Новая
       23

Кодировка церкви для зависимых типов: от Coq до Haskell

4 голосов
/ 09 марта 2019

В Coq я могу определить кодировку Черча для списков длиной n: 

Definition listn (A : Type) : nat -> Type :=
fun m => forall (X : nat -> Type), X 0 -> (forall m, A -> X m -> X (S m)) -> X m.

Definition niln (A : Type) : listn A 0 :=
fun X n c => n.

Definition consn (A : Type) (m : nat) (a : A) (l : listn A m) : listn A (S m) :=
fun X n c => c m a (l X n c).

Достаточно ли сильна система типов Haskell (включая ее расширения) для размещения таких определений?Если да, то как?

1 Ответ

4 голосов
/ 09 марта 2019

Конечно, это: 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

import Data.Kind        -- Needed for `Type`

data Nat = Z | S Nat    -- Roll your own...

type List (a :: Type) (n :: Nat) =
  forall (x :: Nat -> Type). x Z -> (forall (m :: Nat). a -> x m -> x (S m)) -> x n

niln :: List a Z
niln = \z _ -> z

consn :: a -> List a n -> List a (S n)
consn a l = \n c -> c a (l n c)

Еще одно доказательство (для скептиков) изоморфизма с обычной формулировкой ГАДТ: 

data List' (a :: Type) (n :: Nat) where
  Nil :: List' a Z
  Cons :: a -> List' a m -> List' a (S m)

to :: List' a n -> List a n
to Nil = niln
to (Cons a l) = consn a (to l)

from :: List a n -> List' a n
from l = l Nil Cons
...