////////// Exercice _1_ ////////// type empty type nonempty module PList : sig (* The signature / interface of the module *) type 'a plist val nil : empty plist val cons : int -> 'a plist -> nonempty plist val head : nonempty plist -> int end = struct (* The implementation of the module *) type ilist = Nil | Cons of int * ilist type 'a plist = ilist (* Add a phantom type parameter *) let nil = Nil let cons x xs = Cons (x, xs) let head l = match l with | Nil -> assert false (* Never reached *) | Cons (x, _) -> x end;; type zero type 'n succ type ('n, 'a) nlist = 'a list ////////// Exercice _2_ ////////// {-# LANGUAGE GADTs, TypeOperators, StandaloneDeriving #-} data Zero data Succ n data BList size a where -- Lists with encoded length Nil :: BList Zero a -- * empty list Cons :: a -> BList n a -> BList (Succ n) a -- * cons deriving instance Show a => Show (BList size a) -- Allow lists display -- The tail type-safe function (no error case) tail :: BList (Succ n) a -> BList n a tail (Cons x xs) = xs data Nat size where -- Singleton type for Zero and Succ Z :: Nat Zero -- * zero S :: Nat n -> Nat (Succ n) -- * successor deriving instance Show (Nat size) -- Allow Nat display data n :< m where -- Type witness for 'n < m' LessZ :: Zero :< Succ n -- LessZ is a proof that '0 < S x' forall x LessS :: (m :< n) -> Succ m :< Succ n -- LessS is a proof that 'n < m' implies 'S n < S m' deriving instance Show (n :< m) lt :: Nat n -> Nat m -> Maybe (n :< m) lt Z (S n) = Just LessZ lt (S n) (S m) = case lt n m of Just proof -> Just (LessS proof) Nothing -> Nothing lt _ _ = Nothing ////////// Exercice _3_ ////////// {-@ type Even = { v : Int | v mod 2 = 0 } @-} -- Type definition {-@ weAreEven :: [Even] @-} -- Liquid Haskell annotation weAreEven :: [Int] -- Plain Haskell annotation weAreEven = [-10, 4, 0, 2, 666] {-@ isEven :: Nat -> Bool @-} isEven :: Int -> Bool isEven 0 = True isEven 1 = False isEven n = not (isEven (n-1)) shift :: [Int] -> Int -> [Int] shift xs k = [x + k | x <- xs] double :: [Int] -> [Int] double xs = [x + x | x <- xs] {-@ range :: lo:Int -> hi:Int -> [{v:Int | (lo <= v && v < hi)}] / [hi-lo] @-} range :: Int -> Int -> [Int] range lo hi | lo < hi = lo : range (lo+1) hi | otherwise = [] evens :: Int -> [Int] evens n = [i | i <- range 0 n, isEven i] {-@ type NotZero = { v:Int | v != 0 } @-} {-@ divide :: Int -> Int -> Int @-} divide :: Int -> Int -> Int divide n d = n `div` d {-@ type ListN a N = { v:[a] | len v == N } @-} {-@ type Btwn Lo Hi = { v:Int | Lo <= v && v < Hi } @-} {-@ type NEList a = { v:[a] | 0 < len v } @-} {-@ avg :: [Int] -> Int @-} avg :: [Int] -> Int avg xs = divide total n where total = sum xs n = length xs {-@ loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a @-} loop :: Int -> Int -> a -> (Int -> a -> a) -> a loop lo hi base f = go2 base lo where {-@ go2 :: a -> {i:Nat | i >= lo } -> a / [hi-i] @-} go2 acc i | i < hi = go2 (f i acc) (i + 1) | otherwise = acc {-@ dotProduct :: x:[Int] -> { y:[Int] | len x = len y } -> Int @-} dotProduct :: [Int] -> [Int] -> Int dotProduct x y = loop 0 sz 0 body where sz = length x body i acc = acc + (x !! i) * (y !! i) nhead :: [a] -> a nhead vec = head vec ntail :: [a] -> [a] ntail l = tail l ////////// Exercice _4_ ////////// Section nat_plus. (* A definition of plus for nat values *) Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (plus p m) end. About plus. Notation "x + y" := (plus x y) (at level 50, left associativity). Check S O + S O. Check 1 + 1. Compute S O + S O. Compute 12 + 13. End nat_plus. Theorem plus_O_n : forall n : nat, 0 + n = n. Proof. intros n. simpl. reflexivity. Qed. Section list_length. Inductive ilist (A : Type) : nat -> Type := | Nil : ilist A O | Cons : forall n, A -> ilist A n -> ilist A (S n). Arguments Nil [A]. Arguments Cons [A] [n] _ _. Inductive fin : nat -> Set := | First : forall n, fin (S n) | Next : forall n, fin n -> fin (S n). Arguments First [n]. Arguments Next [n] _. Fixpoint get A n (ls : ilist A n) : fin n -> A := match ls with | Nil => fun idx => match idx in fin n' return (match n' with | O => A | S _ => unit end) with | First => tt | Next _ => tt end | Cons x ls' => fun idx => match idx in fin n' return (fin (pred n') -> A) -> A with | First => fun _ => x | Next idx' => fun get_ls' => get_ls' idx' end (get _ _ ls') end. Arguments get [A] [n] _ _. End list_length.