edwinb

  joke : Protocol ['A, 'B] ()
  joke = do 'A ==> 'B | Literal "Knock knock"
            'B ==> 'A | Literal "Who's there?"
            name <- 'A ==> 'B | String
            'B ==> 'A | Literal (name ++ " who?")
            'A ==> 'B | (punchline : String **
                            Literal (name ++ punchline))
            Done

edwinb

module Main
  
{- Divide x by y, as long as there is a proof that y is non-zero. The
   'auto' keyword on the 'p' argument means that when safe_div is called,
   Idris will search for a proof. Either y will be statically known, in
   which case this is easy, otherwise there must be a proof in the context.

   'so : Bool -> Type' is a predicate on booleans which only holds if the
   boolean is true. Essentially, we are making it a requirement in the type
   that a necessary dynamic type is done before we call the function -}

edwinb

  data Elem : a -> Vect n a -> Type where
       Here : Elem x (x :: xs)
       There : Elem x xs -> Elem x (y :: xs)
  
  isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)
  isElem x [] = Nothing
  isElem x (y :: xs) with (decEq x y)
    isElem x (x :: xs) | (Yes refl) = Just Here
    isElem x (y :: xs) | (No contra) = Just (There !(isElem x xs))

edwinb

  vapp : Vect n a -> Vect m a -> Vect (m + n) a
  vapp [] ys ?= {vapp_nil_lemma} ys
  vapp (x :: xs) ys ?= {vapp_cons_lemma} x :: vapp xs ys
  
  ---------- Proofs ----------
  
  Main.vapp_cons_lemma = proof
    intros
    rewrite (plusSuccRightSucc m n)
    trivial

edwinb

I can’t help but feel that this is a really misguided effort.

When you start programming with dependent types, as your types get more descriptive you will inevitably end up needing to prove things. Hence, ultimately you will want the system to fulfill the role of a proof assistant, anyway.

It makes no sense, then, to dismiss Coq on the grounds that it is a proof assistant. Yes, it could use some facilities to make it more practical for actual programs. But it is a very mature system, based on a nice rich calculus, with lots of nice infrastructure, a growing standard library, lots of documentation and publications, etc. It makes much more sense to find out what Coq is missing and add it, rather than starting from scratch.

edwinb

  data AltList : a -> b -> Type where
      Nil  : AltList a b
      (::) : b -> AltList a b -> AltList b a
  
  test : AltList String Int
  test = ["hi", 2, "cat", 3, "hoy"]

edwinb

  ones : Num a => Stream a
  ones = 1 :: ones
  
  twos : Num a => Stream a
  twos = 2 :: twos
  
  codata EqStream : Stream a -> Stream a -> Type where
    ReflStream : x = y -> EqStream xs ys -> EqStream (x :: xs) (y :: ys)
  
  -- can't do it for all Num since we don't know how * behaves!

edwinb

data Tree : Nat -> Type -> Type where
     Leaf : Tree Z a
     Node : Tree ln a -> a -> Tree rn a -> Tree (ln + (S rn)) a

insert : Ord a => a -> Tree n a -> Tree (S n) a
insert val Leaf = Node Leaf val Leaf
insert val (Node l x r) with (val <= x)
  insert val (Node l x r) | True = Node (insert val l) x r
  insert val (Node l x r) | False ?= {tree_right} Node l x (insert val r)

edwinb

-- Version 1, no possible failure

  openDoor : { [DOOR Closed] ==> [DOOR Open] } Eff ()
  openDoor = call OpenDoor
  
  closeDoor : { [DOOR Open] ==> [DOOR Closed] } Eff ()
  closeDoor = call CloseDoor
  
  knock : { [DOOR Closed] } Eff ()
  knock = call Knock

edwinb

AnyST : Type -> Type -> Type
AnyST s a = {m : _} -> Monad m => StateT s m a
  
foo : AnyST Integer ()
foo = do x <- get
         put (x + 1)
  
wibble : StateT Integer Maybe ()
wibble = foo