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

  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 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

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

  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

  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

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

  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

import Effects
import Effect.StdIO

import System.Protocol

data Command = Next | SetIncrement | Stop 

count : Protocol ['Client, 'Server] ()

edwinb

  data Strategy : Type where
       MkStrategy : (t : Type -> Type) ->
                    (delay : (a : Type) -> a -> t a) ->
                    (force : (a : Type) -> t a -> a) ->
                    Strategy
  
  strategy : Strategy -> Type -> Type
  strategy (MkStrategy t delay force) = t
  
  delay : {s : Strategy} -> {a : Type} -> a -> strategy s a