0
size
returns positive valuesavg
head
and tail
are Safefoldr1
average
map
init
init'
insert
List
s ElementsList
max
type (I)max
type (II)max
type (III)max
typekeys
Map
eval
create
unsafeTake
unpack
chop
Lets define our own List
data type:
Measure
Haskell function with a single equation per constructor
Measure
Automagically Strengthens type of data constructor
data List a where
Emp :: {v:List a | length v = 0}
(:::) :: x:a -> xs:List a
-> {v:List a | length v = 1 + length xs}
Fear head
and tail
no more!
Q: Write types for head
and tail
that verify impossible
.
A convenient type alias
foldr1
Fold f
over list initially using first element:
average
Q: What is a safe input type for average'
?
Make illegal states unrepresentable
Legal Values: Lists of 12
elements, e.g.
"jan" ::: "feb" ::: ... ::: "dec" ::: Emp"
Refine Type to Legal Values
Lists Of A Given Size
Make illegal states unrepresentable
Refine Type to Legal Values
{-@ data Year a = Year (ListN a 12) @-}
Automagically strengthens type of data constructor
data Year a where
Year :: ListN a 12 -> Year a
map
Q: Can you fix map
to verify tempAverage
?
init
Q: Can you fix the type of init
so that sanDiegoTemp
is accepted?
init'
Q: For bonus points, fix init'
so sanDiegoTemp'
is accepted?
Next: Case Study
init' :: (Int -> a) -> n:Nat -> ListN a n init' f n = go 0 where go :: i:{Nat | i <= n} -> ListN a {n-i} go i | i < n = f i ::: go (i+1) | otherwise = Emp