haskell - (Type) safely retrieving an element of a vector -

i attempting write function

getcolumn :: int -> vector n e -> e 

that retrieves i'th item vector of size n.

these vectors defined follows:

data natural   0 :: natural   succ :: natural -> natural  type 1   = succ 0 type 2   = succ 1 type 3 = succ 2 type 4  = succ 3  data vector n e   nil  :: vector 0 e   (:|) :: e -> vector n e -> vector (succ n) e  infixr :| 

is there way write getcolumn function in way compiler reject code if int big vector's size?

how write function?

first, need singleton type naturals. singletons run-time representations of type-level data, , they're called singleton types because each of them has single value. useful because establishes one-to-one correspondence between values , represented type; knowing either type or value lets infer other.

this lets circumvent limitation haskell types cannot depend on haskell values: our types depend on type index of singleton, type index can in turn determined value of singleton. tortuous detour not present in dependent programming languages such agda or idris, types can depend on values.

data snatural (n :: natural)     szero :: snatural 0     ssucc :: snatural n -> snatural (succ n)   deriving instance show (snatural n) -- requires standalonederiving 

we can see n, snatural n has single possible value; mirrors original natural definition.

there multiple ways can proceed towards vector indexing.

1. defining < constraint directly.

defining < on naturals straightforward:

{-# language typeoperators, typefamilies #-}  type family < b      0   < succ b = true          < 0   = false     succ < succ b = < b   

now can express boundedness type equality constraint:

index :: ((m < n) ~ true) => vector n -> snatural m -> index (x :| xs) szero     = x  index (x :| xs) (ssucc i) = index xs index _         _         = error "impossible"  main =     print $ index (0 :| 1 :| nil) szero -- 0     print $ index (0 :| 1 :| nil) (ssucc (ssucc szero)) -- type error  

2. using alternative representation of naturals baked-in bounds.

this standard solution in dependently typed programming, , imo simpler one, although it's bit more difficult understand @ first. call bounded natural type fin n (for "finite"), n natural representing upper bound. trick index our number in way such size of value can't greater index.

data fin (n :: natural)     fzero :: fin (succ n)     fsucc :: fin n -> fin (succ n)  

it's apparent fin zero doesn't have values. fin (succ zero) has single value, fzero, fin (succ (succ zero)) has 2 values, , fin n has n possible values. can use safe indexing straightforwardly:

index :: vector n -> fin n -> index (x :| xs) fzero     = x index (x :| xs) (fsucc i) = index xs index _         _         = error "impossible"   main =     print $ index (0 :| 1 :| nil) (fsucc (fsucc fzero)) -- type error 

addendum: using singletons library , doing safe indexing int-s.

as we've seen, doing dependent programming in haskell involves hefty amount of boilerplate. type-level data , singletons more or less identical, yet still need separate definitions. functions operating on them have duplicated similarly. luckily, singletons package can generate boilerplate us:

{-# language      typefamilies, gadts, datakinds, polykinds,     scopedtypevariables, templatehaskell #-}  import data.singletons.th  -- "snat n" singleton generated too.  $(singletons[d| data nat = z | s nat |])  data vector n e   nil  :: vector z e   (:|) :: e -> vector n e -> vector (s n) e infixr :|  data fin n     fz :: fin (s n)     fs :: fin n -> fin (s n)   index :: vector n -> fin n -> index (x :| xs) fz     = x index (x :| xs) (fs i) = index xs index _         _      = error "impossible" 

the package includes convenient ways generate singleton values types needed:

foo :: snat (s (s (s z))) foo = sing 

sing polymorphic value may serve stand-in singleton value. correct value can inferred context, other times have annotate type index, using scopedtypevariables extension.

now can index safely int-s without being overmuch bothered boilerplate (not catastrophic amount of boilerplate though; implementing sing nat hand require 1 more typeclass , couple of instances).

in general, verified programming not validating data compile time (as we've seen in examples above), rather writing functions operate in provably correct way, on data unknown compile-time (you it's irrelevant when validate data, provided validation functions correct). our index can viewed semi-verified function, because impossible implement error-throwing version of typechecks (modulo bottoms , divergence).

to safely index int-s, have write verified conversion function int fin, , use index usual:

checkbound :: int -> snat n -> maybe (fin n) checkbound _ | < 0 = nothing checkbound 0 (ss _)    = fz checkbound sz        = nothing checkbound (ss n)    = case checkbound (i - 1) n of     n -> (fs n)     nothing -> nothing 

again, magic of checkbound is impossible write definition returns fin violates given bound.

indexint :: forall n . singi n => vector n -> int -> maybe indexint v = case checkbound (sing :: snat n) of      -> (index v i)     nothing -> nothing 

here need utilize singletons machinery: singi constraint allows conjure appropriate singleton value using sing. it's harmless class constraint, because every possible n instance of singi, construction.