Dependently Typed Programming in Idris: A Demo

 1 module Demo
 2 
 3 %default total
 4 
 5 data Nat' : Type where
 6   Z' : Nat'
 7   S' : Nat' -> Nat'
 8 
 9 %name Nat' n,m,o
10 
11 plus' : Nat' -> Nat' -> Nat'
12 plus' Z'     m = m
13 plus' (S' n) m = S' (plus' n m)
14 
15 data Vect' : Nat -> Type -> Type where
16   Nil : Vect' Z a
17   (::) : a -> Vect' n a -> Vect' (S n) a
18 
19 %name Vect' xs,ys,zs
20 
21 append : Vect' n a -> Vect' m a -> Vect' (n + m) a
22 append Nil       ys = ys
23 append (x :: xs) ys = x :: (append xs ys)
24 
25 zip : Vect' n a -> Vect' n b -> Vect' n (a, b)
26 zip []        []        = []
27 zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
28 
29 take' : (n : Nat) -> Vect (n + m) a -> Vect n a
30 take' Z     xs = []
31 take' (S k) (x :: xs) = x :: take' k xs
32 
33 drop' : (n : Nat) -> Vect (n + m) a -> Vect m a
34 drop' Z xs = xs
35 drop' (S k) (x :: xs) = drop' k xs
36 
37 
38 data SnocList : List a -> Type where
39   SnocNil : SnocList (Nil {a=a})
40   Snoc    : (xs : List a) -> (x :a) -> SnocList (xs ++ [x])
41 
42 snocced : (xs : List a) -> SnocList xs
43 snocced [] = SnocNil
44 snocced (x :: xs) with (snocced xs)
45   snocced (x :: [])          | SnocNil     = Snoc [] x
46   snocced (x :: (ys ++ [y])) | (Snoc ys y) = Snoc (x :: ys) y
47 
48 rot : Nat -> List a -> List a
49 rot Z       xs                        = xs
50 rot (S k)   xs       with (snocced xs)
51   rot (S k) []          | SnocNil     = []
52   rot (S k) (ys ++ [x]) | (Snoc ys x) = rot k (x::ys)

  1 module AVL
  2 
  3 %default total
  4 -------------------------------------------
  5 -- AVL trees
  6 
  7 
  8 
  9 data Balance : Nat -> Nat -> Type where
 10   LeftLeaning  : Balance (S n) n
 11   RightLeaning : Balance n (S n)
 12   Balanced     : Balance n n
 13 
 14 %name Balance b, bal
 15 
 16 
 17 total
 18 height : Balance n m -> Nat
 19 height (LeftLeaning {n}) = S (S n)
 20 height (RightLeaning {n}) = S (S n)
 21 height {n} (Balanced {n}) = S n
 22 
 23 
 24 data Tree : Nat -> Type -> Type -> Type where
 25   Empty : Tree 0 k v
 26   Node : (l : Tree n k v) ->
 27          (key : k) -> (val : v) ->
 28          (r : Tree m k v) ->
 29          (b : Balance n m) -> Tree (height b) k v
 30 
 31 %name Tree t, tree
 32 
 33 
 34 
 35 
 36 -- Bad tree:
 37 -- Node Empty 0 "0" (Node Empty 1 "1" (Node Empty 2 "2" Empty RightLeaning) RightLeaning) RightLeaning
 38 
 39 lookup : (Ord k) => k -> Tree n k v -> Maybe v
 40 lookup x Empty = Nothing
 41 lookup x (Node l key val r b) =
 42   case compare x key of
 43     LT => lookup x l
 44     EQ => Just val
 45     GT => lookup x r
 46 
 47 
 48 
 49 
 50 
 51 
 52 data InsertRes : Nat -> Type -> Type -> Type where
 53   Flat : Tree n k v -> InsertRes n k v
 54   Taller : Tree (S n) k v -> InsertRes n k v
 55 
 56 %name InsertRes res, r
 57 
 58 
 59 rotLeft : Tree n k v -> k -> v -> Tree (S (S n)) k v -> InsertRes (S (S n)) k v
 60 
 61 -- Impossible because Empty has depth 0 and we know the depth is at least 2 from the type
 62 rotLeft l key val Empty impossible
 63 
 64 rotLeft l key val (Node rl key' val' rr Balanced) =
 65   Taller $ Node (Node l key val rl RightLeaning) key' val' rr LeftLeaning
 66 
 67 rotLeft l key val (Node (Node rll key'' val'' rlr LeftLeaning) key' val' rr LeftLeaning) =
 68   Flat $ Node rll key'' val'' (Node rlr key' val' rr RightLeaning) RightLeaning
 69 
 70 rotLeft l key val (Node (Node rll key'' val'' rlr RightLeaning) key' val' rr LeftLeaning) =
 71   Flat $ Node (Node l key val rll LeftLeaning) key'' val'' (Node rlr key' val' rr Balanced) Balanced
 72 
 73 rotLeft l key val (Node (Node rll key'' val'' rlr  Balanced) key' val' rr LeftLeaning) =
 74   Flat $ Node (Node l key val rll Balanced) key'' val'' (Node rlr key' val' rlr Balanced) Balanced
 75 
 76 rotLeft l key val (Node rl key' val' rr RightLeaning) =
 77   Flat $ Node  (Node  l key val rl Balanced) key' val' rr Balanced
 78 
 79 
 80 
 81 rotRight : Tree (S (S n)) k v -> k -> v -> Tree n k v -> InsertRes (S (S n)) k v
 82 rotRight Empty key val r impossible
 83 
 84 rotRight (Node ll key val (Node lrl key' val' lrr RightLeaning) RightLeaning) key'' val'' r =
 85   Flat $ Node (Node ll key val lrl LeftLeaning) key' val' (Node lrr key'' val'' r Balanced) Balanced
 86 
 87 rotRight (Node ll key val (Node lrl key' val' lrr LeftLeaning) RightLeaning) key'' val'' r =
 88   Flat $ Node (Node ll key val lrl Balanced) key' val' (Node lrr key'' val'' r RightLeaning) Balanced
 89 
 90 rotRight (Node ll key' val' lr Balanced) key val r =
 91   Taller $ Node ll key' val' (Node lr key val r LeftLeaning) RightLeaning
 92 
 93 rotRight (Node ll key' val' lr LeftLeaning) key val r =
 94   Flat $ Node ll key' val' (Node lr key val r Balanced) Balanced
 95 
 96 rotRight (Node ll key' val' (Node lrl key'' val'' lrr Balanced) RightLeaning) key val r =
 97   Flat $ Node (Node ll key' val' lrl Balanced) key'' val'' (Node lrr key val r Balanced) Balanced
 98 
 99 
100 insert : (Ord k) => k -> v -> (t : Tree n k v) -> InsertRes n k v
101 insert newKey newVal Empty = Taller (Node Empty newKey newVal Empty Balanced)
102 insert newKey newVal (Node l key val  r b) with (compare newKey key)
103   insert newKey newVal (Node l key val r b) | EQ = Flat (Node l newKey newVal r b)
104   insert newKey newVal (Node l key val r b) | LT with (insert newKey newVal l)
105     insert newKey newVal (Node l key val r b)            | LT | (Flat l')   = Flat (Node l' key val r b)
106     insert newKey newVal (Node l key val r LeftLeaning)  | LT | (Taller l') = rotRight l' key val r
107     insert newKey newVal (Node l key val r Balanced)     | LT | (Taller l') = Taller (Node l' key val r LeftLeaning)
108     insert newKey newVal (Node l key val r RightLeaning) | LT | (Taller l') = Flat (Node l' key val r Balanced)
109   insert newKey newVal (Node l key val r b) | GT with (insert newKey newVal r)
110     insert newKey newVal (Node l key val r b)            | GT | (Flat r')   = Flat (Node l key val r' b)
111     insert newKey newVal (Node l key val r LeftLeaning)  | GT | (Taller r') = Flat (Node l key val r' Balanced)
112     insert newKey newVal (Node l key val r Balanced)     | GT | (Taller r') = Taller (Node l key val r' RightLeaning)
113     insert newKey newVal (Node l key val r RightLeaning) | GT | (Taller r') = rotLeft l key val r'
114 
115 
116 fromList : Ord k => List (k, v) -> (n : Nat ** Tree n k v)
117 fromList [] = (0 ** Empty)
118 fromList ((k, v) :: xs) with (insert k v (getProof (AVL.fromList xs)))
119   fromList ((k, v) :: xs) | (Flat x) = (_ ** x)
120   fromList ((k, v) :: xs) | (Taller x) = (_ ** x)
121 
122 
123 flatten : Tree n k v -> List (k, v)
124 flatten Empty = []
125 flatten (Node l key val r b) = flatten l ++ [(key, val)] ++ flatten r
126 
127 
128 tree1 : Tree 1 Int Int
129 tree1 = Node Empty 0 0 Empty (Balanced {n = 0})
130 
131 
132 
133 
134 test : InsertRes 3 Int Int
135 test =
136   let key : Int = 0 in let key' : Int = 0 in let key'' : Int = 0 in
137   let val : Int = 0 in let val' : Int = 0 in let val'' : Int = 0 in
138   let l : Tree 1 Int Int = tree1 in
139   let rll : Tree 1 Int Int = tree1 in
140   let rlr : Tree 0 Int Int = Empty in
141   let rr : Tree 1 Int Int = tree1 in
142   let rl : Tree 2 Int Int = Node rll key'' val'' rlr LeftLeaning in
143   let r : Tree 3 Int Int = (Node rl key' val' rr (the (Balance 2 1) LeftLeaning)) in
144   let res = rotLeft l 0 0 r in
145   res
146 

 1 module Universes
 2 
 3 %default total
 4 
 5 data Sizable = INT | LIST Sizable | EITHER Sizable Sizable
 6 
 7 interp : Sizable -> Type
 8 interp INT = Int
 9 interp (LIST x) = List (interp x)
10 interp (EITHER x y) = Either (interp x) (interp y)
11 
12 
13 size : (t : Sizable) -> interp t -> Int
14 size INT x = x
15 size (LIST y) xs = sum (map (size y) xs)
16 size (EITHER y z) (Left x) = 1 + size y x
17 size (EITHER y z) (Right x) = 1 + size z x
18 

 1 module Interpreter
 2 
 3 %default total
 4 
 5 infixr 6 ==>
 6 
 7 data Ty = BOOL | (==>) Ty Ty
 8 
 9 %name Ty t,u
10 
11 typeOf : Ty -> Type
12 typeOf BOOL = Bool
13 typeOf (t ==> u) = typeOf t -> typeOf u
14 
15 using (n : Nat, ctxt : Vect n Ty)
16   data Term : Vect n Ty -> Ty -> Type where
17     T : Term ctxt BOOL
18     F : Term ctxt BOOL
19     IF : Term ctxt BOOL -> Term ctxt t -> Term ctxt t -> Term ctxt t
20 
21     App : Term ctxt (t ==> u) -> Term ctxt t -> Term ctxt u
22     Lam : Term (t::ctxt) u -> Term ctxt (t ==> u)
23     Var : (i : Fin n) -> Term ctxt (index i ctxt)
24 
25   %name Term tm, tm', tm''
26 
27   not : Term ctxt (BOOL ==> BOOL)
28   not = Lam $ IF (Var 0) F T
29 
30   choose : Term ctxt (BOOL ==> BOOL ==> BOOL ==> BOOL)
31   choose = Lam $ Lam $ Lam $ IF (Var 2) (Var 1) (Var 0)
32 
33   not' : Term ctxt (BOOL ==> BOOL)
34   not' = Lam (App (App (App choose (Var 0)) F) T)
35 
36   data Env : Vect n Ty -> Type where
37     Nil : Env []
38     (::) : typeOf t -> Env ctxt -> Env (t::ctxt)
39 
40   lookup : (i : Fin n) -> (env : Env ctxt) -> typeOf (index i ctxt)
41   lookup fZ (x :: y) = x
42   lookup (fS x) (y :: z) = lookup x z
43 
44   eval : Term ctxt t -> Env ctxt -> typeOf t
45   eval T env = True
46   eval F env = False
47   eval (IF tm tm' tm'') env = if eval tm env then eval tm' env else eval tm'' env
48   eval (App f x) env = (eval f env) (eval x env)
49   eval (Lam tm) env = \ x => eval tm (x :: env)
50   eval (Var i) env = lookup i env
51 
52 
53