edwinb

Ran ffi001...FAILURE
2c2
< 0.9995736030415051 : Float
---
0.9995736030415051 : Float
make[1]: *** [ffi001.test] Error 1

edwinb

(./DB/SQLite/SQLiteNew.idr:19:13,"Type\n")
(./DB/SQLite/SQLiteNew.idr:19:13,"Type\n")
(./DB/SQLite/SQLiteNew.idr:20:13,"List (List DBVal)\n")
(./DB/SQLite/SQLiteNew.idr:20:19,"List DBVal)\n")
(./DB/SQLite/SQLiteNew.idr:22:10,"Type\n")
(./DB/SQLite/SQLiteNew.idr:22:10,"Type\n")
(./DB/SQLite/SQLiteNew.idr:23:10,"String\n")
(./DB/SQLite/SQLiteNew.idr:25:15,"Type\n")
(./DB/SQLite/SQLiteNew.idr:25:15,"Type\n")
(./DB/SQLite/SQLiteNew.idr:26:15,"String\n")

edwinb

class Marshal val chan where
      sendType : Type -> Type
      recvType : Type -> Type

      marshal   : val -> sendType val
      unmarshal : sendType val -> recvType val

edwinb

foo : (xs : Vect n a) -> (ys : Vect m a) -> ?noIdea
foo xs ys = xs ++ ys

Currently this gives:

Can't unify
        Vect (n + m) a
with
        ?noIdea

edwinb

Keybase proof

I hereby claim:

• I am edwinb on github.
• I am edwinb (https://keybase.io/edwinb) on keybase.
• I have a public key whose fingerprint is 9FDE 3D18 203F 0CFA DD7A A817 F219 A102 9E17 61E3

To claim this, I am signing this object:

edwinb

@article{JFP:9060502,
author = {BRADY,EDWIN},
title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
journal = {Journal of Functional Programming},
volume = {23},
issue = {05},
month = {9},
year = {2013},
issn = {1469-7653},
pages = {552--593},

edwinb

-- We could define the relation like this:

data LessThan : Nat -> Nat -> Type where
     LT_Z : LessThan Z (S m)
     LT_S : LessThan n m -> LessThan (S n) (S m)

-- Then calculate a proof, if one exists:
  
isLessThan : (m : Nat) -> (n : Nat) -> Maybe (LessThan m n)
isLessThan Z Z = Nothing

edwinb

  record Person : Nat -> Type where
         MkPerson : (name : String) ->
                    (age : Nat) ->
                    Person age
  
  record Event : Type where
         MkEvent : (name : String) -> (organiser : Person a) -> Event
  
  record Meeting : Int -> Type where
         MkMeeting : (event : Event) ->

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

edwinb

module Main

import Effects
import Effect.StdIO

import System.Protocol

data Command = Next | SetIncrement | Stop 

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