{-# LANGUAGE GADTs, TypeFamilies #-}
__module__ Types __where__
__data__ Zero
__data__ Suc n
__data__ Vec a n __where__
Nil :: Vec a Zero
Cons :: a -> Vec a n -> Vec a (Suc n)
__type__ family Add m n :: *
__type__ __instance__ Add Zero n = n
__type__ __instance__ Add (Suc m) n = Suc (Add m n)
{- Task (a): Give the signature and implementation of |(++)| for
vector concatenation and explain why it type checks. -}
(+++) :: Vec a m -> Vec a n -> Vec a (Add m n)
Nil +++ ys = ys
Cons x xs +++ ys = Cons x (xs +++ ys)
-- Nil :: Vec a Zero
-- return type = Vec a (Add Zero n) = Vec a n = the type of ys
-- Cons x xs :: Vec a (Suc m)
-- return type = Vec a (Add (Suc m) n) = Vec a (Suc (Add m n)) = type of the RHS
{- Would it still type check with the alternative definition of
type-level addition below? Why/why not?
-}
__type__ family Add' m n :: *
__type__ __instance__ Add' m Zero = m
__type__ __instance__ Add' m (Suc n) = Suc (Add' m n)
{- No, it would not type check. The case split in the function
definition must match the case split in the type family, otherwise the
type unification will fail. It is possible to work around it using a
family for type equality and a coerce function. -}
-- Task (b): Implement a GADT |Fin n| for unary numbers below |n| and
-- a lookup function |(!) :: Vec a n -> Fin n -> a|.
__data__ Fin n __where__
Fzero :: Fin (Suc n)
Fsuc :: Fin n -> Fin (Suc n)
(!) :: Vec a n -> (Fin n -> a)
Cons x xs ! Fzero = x
Cons x xs ! (Fsuc i) = xs ! i
{- Task (c): Briefly explain the Curry-Howard correspondence for
``false'', ``true'', ``implies'', ``and'', ``or''.
----
The Curry-Howard correspondence provides a "Logic" reading of types:
Types Logic
p :: P p is a proof of P
empty type False
non-empty type True
P -> Q P implies Q
(P, Q) P and Q
Either P Q P or Q
-- Not asked for in the exam:
(a :: A) -> P ∀a:A. P -- dependent function type
(a :: A, P) ∃a:A. P -- dependent pair type
-}
-- ................
-- Test code - not part of the exam
v1 = Cons 1 (Cons 7 Nil)
v2 = Cons 3 (Cons 8 Nil)
long = v1 +++ v2
two = Fsuc (Fsuc Fzero)
main = print (long ! two == 3)