{-# 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)