# Code (Week 8)

## Table of Contents

## 1 Sized Vectors

Some more examples on sized vectors, inculding some requiring explitic casts to type check. I won't expect anyone to be able to write such a program with explicit casts in the exam, but you should understand which types can be checked automatically, and the limits of sized vectors.

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-} module Vector where import Data.Proxy import Data.Type.Equality import Prelude hiding ((++)) data Nat = Z | S Nat type family (+) (n :: Nat) (m :: Nat) :: Nat type instance 'Z + m = m type instance ('S n) + m = 'S (n + m) data SNat (n :: Nat) where Zero :: SNat Z Succ :: SNat m -> SNat (S m) data Vec a (n :: Nat) where Nil :: Vec a 'Z (:::) :: a -> Vec a n -> Vec a ('S n) deriving instance Show a => Show (Vec a n) vHead :: Vec a ('S n) -> a vHead (x ::: xs) = x vTail :: Vec a ('S n) -> Vec a n vTail (x ::: xs) = xs vMap :: (a -> b) -> Vec a n -> Vec b n vMap f Nil = Nil vMap f (x ::: xs) = (f x) ::: (vMap f xs) -- can't return a sized vector, as number of output elements -- unknown. removeOdd :: Vec Int n -> [Int] removeOdd Nil = [] removeOdd (x ::: xs) | odd x = removeOdd xs cd | otherwise = x : (removeOdd xs) (++) :: Vec a n -> Vec a m -> Vec a (n + m) Nil ++ xs = xs (x ::: xs) ++ ys = x ::: (xs ++ ys) {- optional exercise: replace the XXX with theorems given below to get reverse to type check (the type error message which you get when removing gcastWith XXX will tell you what's missing) vReverse :: Vec a n -> Vec a n vReverse vs = gcastWith XXX $ rev' vs Nil where rev' :: Vec a n -> Vec a m -> Vec a (n + m) rev' Nil ws = ws rev' (v ::: vs) ws = gcastWith XXX $ rev' vs (v ::: ws) -} merge :: Vec Int n -> Vec Int m -> Vec Int (n + m) merge Nil ys = ys merge xs Nil = gcastWith (plus_id_rv xs) xs merge v1@(x ::: xs) v2@(y ::: ys) | x <= y = x ::: (merge xs v2) | otherwise = gcastWith (plus_succ_idv v1 ys) (y ::: (merge v1 ys)) plus_id_rv :: Vec a n -> ((n + Z) :~: n) plus_id_rv Nil = Refl plus_id_rv (x ::: xs) = gcastWith (plus_id_rv xs) Refl -- type level proof that (Vec a (n + (S m)) ~ Vec a (S (n + m)) plus_succ_idv :: Vec a n1 -> Vec a n2 -> ((n1 + (S n2)) :~: (S (n1 + n2))) plus_succ_idv Nil ws = Refl plus_succ_idv (v ::: vs) ws = gcastWith (plus_succ_idv vs ws) Refl -- type level proof that n + (S m)) ~ S (n+ m) plus_succ_id :: SNat n1 -> SNat n2 -> ((n1 + (S n2)) :~: (S (n1 + n2))) plus_succ_id Zero n = Refl plus_succ_id (Succ x) n = gcastWith (plus_succ_id x n) Refl plus_id_r :: SNat n -> ((n + Z) :~: n) plus_id_r Zero = Refl plus_id_r (Succ n) = gcastWith (plus_id_r n) Refl {- Example of a more complex proof: Could be done more compactly, but this way, every step is explicit and corresponds to the proof you would do on paper transitivity combines two equalities: trans:: a :~: b) -> (b :~: c) -> (a :~: c) Induction step: I.H.: n1 + n2 = n2 + n1 Sn1 + n2 = {def of + } S(n1 + n2) = I.H. S(n2 + n1) = {plus_succ_id} (n2 + Sn1) -} -- proof that + is commutative plus_comm :: SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1)) plus_comm Zero m = gcastWith (plus_id_r m) Refl plus_comm (Succ n) m = step4 n m plus_comm step4 :: SNat n1 -> SNat n2 -> (SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))) -> ((S n1 + n2) :~: (n2 + S n1)) step4 n m ih = trans (step2 n m ih) (step3 n m) step3 :: SNat n1 -> SNat n2 -> (S(n2 + n1) :~: (n2 + S (n1))) step3 n m = (sym (plus_succ_id m n)) step2 :: SNat n1 -> SNat n2 -> (SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))) -> (((S n1) + n2) :~: (S(n2 + n1))) step2 n m indHyp = trans Refl (step1 n m indHyp) step1 :: SNat n1 -> SNat n2 -> (SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))) -> (S(n1 + n2) :~: (S(n2 + n1))) step1 n m indHyp = apply Refl (indHyp n m) -- lifts a type equality on SNats to Vecs vec_lift:: (SNat n -> (k :~: l)) -> Vec a n -> (Vec a k :~: Vec a l) vec_lift fn v = apply Refl (fn (len v)) where len ::Vec a n -> SNat n len Nil = Zero len (x ::: xs) = Succ (len xs) vec_lift2:: (SNat n -> SNat m -> (k :~: l)) -> Vec a n -> Vec a m -> (Vec a k :~: Vec a l) vec_lift2 fn v w = apply Refl (fn (len v) (len w)) where len ::Vec a n -> SNat n len Nil = Zero len (x ::: xs) = Succ (len xs)

## 2 Subvectors (optional)

The removeOdd function in the previous example code returns a list, as the size of the result can't be determined just by looking at the size of the input vector. See below for an alternative implementation, which encodes the fact the result is at most as big as the argument in the type. In practice, this is a pretty weak assertion, and in most cases, it wouldn't be worthwhile to go the extra length to encode it in the type.

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {-# FlexibleContexts #-} module EvenV where data Nat = Z | S Nat data Vec a (n :: Nat) where Nil :: Vec a Z (:::) :: a -> Vec a n -> Vec a (S n) class LTE (m :: Nat) (n :: Nat) where instance LTE Z Z where instance LTE Z (S n) where instance LTE m n => LTE (S m) (S n) where instance {-# OVERLAPS #-} LTE m n => LTE m (S n) data SubVec a (n :: Nat) where SV :: LTE m n => Vec a m -> SubVec a n svcons :: a -> SubVec a n -> SubVec a (S n) svcons x (SV xs) = SV (x ::: xs) svup :: SubVec a n -> SubVec a (S n) svup (SV xs) = SV xs removeOdd :: Vec Int n -> SubVec Int n removeOdd Nil = SV Nil removeOdd (x ::: xs) | even x = svcons x (removeOdd xs) | otherwise = svup (takeEven xs)