Skip to content

Instantly share code, notes, and snippets.

@nvanderw
Created March 19, 2014 06:14
Show Gist options
  • Save nvanderw/9636359 to your computer and use it in GitHub Desktop.
Save nvanderw/9636359 to your computer and use it in GitHub Desktop.
Finite sets and safe list indexing
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
data Nat = Zero | Succ Nat
-- Bounded naturals
data Fin :: Nat -> * where
FZ :: Fin (Succ n)
FS :: Fin n -> Fin (Succ n)
data Vect (n :: Nat) a where
Nil :: Vect Zero a
Cons :: a -> Vect n a -> Vect (Succ n) a
-- Type-safe list index lookup
(!) :: Vect n a -> Fin n -> a
(Cons x _) ! FZ = x
(Cons _ xs) ! (FS n) = xs ! n
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! FZ
'f'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS FZ)
'o'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS $ FZ)
'o'
*Main> (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)
<interactive>:14:43:
Couldn't match type 'Succ n0 with 'Zero
Expected type: Fin ('Succ ('Succ ('Succ 'Zero)))
Actual type: Fin ('Succ ('Succ ('Succ ('Succ n0))))
In the second argument of `(!)', namely `(FS . FS . FS $ FZ)'
In the expression:
(Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)
In an equation for `it':
it = (Cons 'f' . Cons 'o' . Cons 'o' $ Nil) ! (FS . FS . FS $ FZ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment