My links:

edit

Start of topic | Skip to actions

Homeworks for Joseph Young

Functions on Sized Lists

The following set of functions are designed to work on sized lists. Sized lists are polymorphic list where the size of the list is built in as a type. We use this more powerful datatype to prevent certain errors, such indexing errors, as well as create faster code. Since we can insure that size constraints are satisified at compile time, our resulting functions will be faster.

Basic Definition

The basic definition of a sized list in Concoqtion is given by

type ('n:'(nat),'a) listl =
| Nil : ('(0),'a) listl
| Cons of let 'm:'(nat) in 'a * ('(m),'a) listl
: ('(1+m),'a) listl

Normally, we will provide an alternative definition without dependent types that can be defined in OCaml. In this case, we will choose to use the builtin list operators.

Sized List Map

Recall the definition of zip defined on regular OCaml lists

let rec my_map2 f l=
    match l with
    | [] -> []
    | x::xs ->
        (f x)::(my_map2 f xs)
;;

We can modify this definition by adding size information to our references to the list. The resulting definition is given by

let rec my_map .|m:'(nat)| (f:'a->'b) (l:('(m),'a) listl):('(m),'a) listl=
    match l in ('(m),'a) listl with
    | Nil -> Nil
    | Cons .|i:'(nat)| (x,xs) ->
        Cons .|'(i)| ((f x),(my_map .|'(i)| f xs))

Sized List Zip

Recall the definition of the zip function given by

let rec my_zip2 l1 l2=
    match (l1,l2) with
    | ([],_) ->
        []
    | (_,[]) ->
        []
    | (x::xs,y::ys) ->
        (x,y)::(my_zip2 xs ys)
;;

Again, we simply add size information to create a function that operates on sized lists. However, notice that we have fewer cases since it can never be the case that the two lists are different sizes.

let rec my_zip .|n:'(nat)| (l1:('(n),'a) slist) (l2:('(n),'b) slist)
    : (('(n),('a * 'b)) slist) =
    match (l1,l2) in ('(n),'a*'b) slist with
    | Nil,Nil -> Nil
    | Cons .|i:'(nat)| (x,xs), Cons .|j:'(nat)| (y,ys) ->
        Cons .|'(j)| ((x,y), my_zip .|'(i)| xs ys)

Concoqtion is actually a fair amount of work behind the scenes in order to make this function easier to write. Without context refinement, this function would be far more complicated. The problem is that although we know that l1 and l2 have the same size when we enter the function, the match statement can not synthesize this information. Thus, the match statement views l1 and l2 to have different sizes until we provide a proof that they are the same. Without context refinement, the definition of my_zip becomes

let cast .|m:'(nat),n:'(nat),p:'(m=n)| (x: ('(m),'a) slist) : ('(n),'a) slist = Obj.magic x;;

let rec my_zip_noc .|n:'(nat)| (l1:('(n),'a) slist) (l2:('(n),'b) slist)
    : (('(n),('a * 'b)) slist) =
    (match (l1,l2)
        as ('m:'(nat),'a) slist * ('n:'(nat),'b) slist
        in forall p:'(m=n). unit -> ('(n),'a*'b) slist with
    | Nil,Nil -> /\p:'(0=0). fun () -> Nil
    | Cons .|i:'(nat)| (x,xs), Cons .|j:'(nat)| (y,ys) ->
        /\p:'(i=j). fun () ->
        let xs'=cast .|'(i), '(j), '(p)| xs in
        Cons .|'(j)| ((x,y), my_zip .|'(j)| xs' ys)     
    ) .|'(refl_equal n)| ()

Sized List Example

We can construct a simple list in the following manner

let x=Cons .|'(0)| (17,Nil);;
let y=Cons .|'(1)| (37,x);;
let z=Cons .|'(2)| (2,y);;

which Concoqtion gives

# z;;
- : ('(S
         ((fix plus (n m : nat) {struct n} : nat :=
             match n with
             | O => m
             | S p => S (plus p m)
             end) 0 2)),
     int)
    listl
= Cons (2, Cons (37, Cons (17, Nil)))

as a return.

Converting a Regular List into a Size List and Existentials

Unfortunately, we don't have sized lists built into Concoqtion. Thus, we lack utility functions that we use with regular lists. We need to write a function that converts an unsized list into a sized list. We can accomplish this with the following code

type ('a) exists_size=E of let 'n:'(nat) in ('(n),'a) listl

let rec size_it (xs:'a list) : ('a exists_size)=
    match xs with
        | [] ->
            E .|'(0)| Nil
        | x::xs ->
            let rest=size_it xs in
            match rest as 'a exists_size in 'a exists_size with
            | E .|n:'(nat)| rest->
                E .|'(1+n)| (Cons .|'(n)| (x,rest))
;;

This illustrates an important concept. The return type for size_it should be there_exists n. (n,'a):listl. Unfortunately, we don't have existentials built into Concoqtion. We can't simply fix the return type to (n,'a) listl since this requires us to know the size of the returned list a priori. Fortunately, we can work around this by creating the datatype exists_size. This allows the size information to be encapsulated into the datatype. Although, it is important to note that since we don't return a sized list, we must structure our code different. For example, say we wanted to zip a sized list with itself where the size list was created from size_it, we have to write a function similar to

let _ =match (size_it x) as 'a exists_size in unit with
    | E .|n:'(nat)| slist->
        let _ = my_zip .|'(n)| slist slist in
        ()
;;

In other words, in order to access the sized list, we have to tear apart the datatype that contains it with a match statement. Then, we can only use this sized list within the scope of the match since the size information is only known within this scope.

Benchmark and Comparison of Sized Lists Versus Regular Lists

Next, we test the efficiency of functions that operate on sized lists versus unsized lists. Our intution tells us that functions that operate on sized lists should be faster since we don't need to write code that verifies the size of the list. The code that sets up the benchmark is given by

let range a b=
    let rec driver a b my_list=
        if a>b then
            my_list
        else
            driver (a+1) b (a::my_list)
    in
    List.rev (driver a b [])
;;

(* Regular order *)
let x=range 1 15000;; 
let _ =match (size_it x) as 'a exists_slist in unit with
    | E_slist .|n:'(nat)| my_slist->
        let _ = Trxtime.timenew
            "Sized Zip" (fun _ -> my_zip .|'(n)| my_slist my_slist) in
        let _ = Trxtime.timenew
            "Sized Map (add1)"
            (fun _ -> my_map .|'(n)| (fun x->x+1) my_slist) in
        let _ = Trxtime.timenew
            "Sized Map (square)"
            (fun _ -> my_map .|'(n)| (fun x->x*x) my_slist) in
        ()
;;
let _ =Trxtime.timenew "Regular Zip" (fun _ -> my_zip2 x x);;
let _ =Trxtime.timenew "Regular Map (add1)" (fun _ -> my_map2 (fun x->x+1) x);;
let _ =Trxtime.timenew "Regular Map (square)" (fun _ ->my_map2 (fun x->x*x) x);;

(* Reverse order *)
let _ =Trxtime.timenew "Regular Zip (b)" (fun _ -> my_zip2 x x);;
let _ =Trxtime.timenew "Regular Map (add1) (b)"
   (fun _ -> my_map2 (fun x->x+1) x);;
let _ =Trxtime.timenew "Regular Map (square) (b)"                                   
   (fun _ ->my_map2 (fun x->x*x) x);;
let _ =match (size_it x) as 'a exists_slist in unit with
    | E_slist .|n:'(nat)| my_slist->
        let _ = Trxtime.timenew
            "Sized Zip (b)" (fun _ -> my_zip .|'(n)| my_slist my_slist) in
        let _ = Trxtime.timenew
            "Sized Map (add1) (b)"
            (fun _ -> my_map .|'(n)| (fun x->x+1) my_slist) in
        let _ = Trxtime.timenew
            "Sized Map (square) (b)"
            (fun _ -> my_map .|'(n)| (fun x->x*x) my_slist) in
        ()
;;

Trxtime.print_times ();;

This has running time

__ Sized Zip __________________ 32x avg= 3.179940E+01 msec
__ Sized Zip (b) ______________ 32x avg= 3.146089E+01 msec
__ Regular Zip ________________ 32x avg= 3.133006E+01 msec
__ Regular Zip (b) ____________ 32x avg= 3.143508E+01 msec
__ Sized Map (add1) ___________ 64x avg= 1.594291E+01 msec
__ Sized Map (add1) (b)________ 64x avg= 1.630496E+01 msec
__ Regular Map (add1) (________ 64x avg= 1.601960E+01 msec
__ Regular Map (add1) _________ 64x avg= 1.601042E+01 msec
__ Sized Map (square) _________ 64x avg= 1.708458E+01 msec
__ Sized Map (square) (________ 64x avg= 1.588681E+01 msec
__ Regular Map (square)________ 64x avg= 1.575679E+01 msec
__ Regular Map (square)________ 64x avg= 1.651263E+01 msec

Counter to our intuition, we can see that there's not really much difference between the two.

Walid: Very good writeup! You might want to also document simple functions like map and fold, and make sure that they are easy enough to write. You might also want to tabulate results of performance numbers collected.

Constructing a Sized List from the First n Elements of a Regular List

Next, we consider the at_size function. This function takes an unsized list and a natural number. Then it returns a sized list of the given size. When the specified size is greater than the size of the original list, we need to signal an error. In order to do this gracefully, we need to introduce a new type that either contains something or nothing:

type 'a my_option=None | Some of 'a;;

In other words, when there's an error we will return None. When the program is successful, we return some. The following programs implements the at_size function. Notice that we have to specially check when n<0. It would be nice to verify this automatically with snats, but the syntax becomes very heavy handed

let at_size (l: 'a list) (n: int) : ('a exists_slist) my_option =
    let rec driver (l: 'a list) (n: int) : ('a exists_slist) my_option =
        match (l, n) as ('a list * int) in ('a exists_slist) my_option with
        | (_, 0) -> Some (E_slist .|'(0)| Nil)
        | ([], m) -> None
        | (x::xs, m) -> let ls = driver xs (n-1) in
        (match ls as ('a exists_slist) my_option    
            in ('a exists_slist) my_option with
            | None -> None                                                                  
            | Some (E_slist .|k:'(nat)| y) ->                                                   
                Some (E_slist .|'(1+k)| (Cons .|'(k)| (x, y))))
    in  
    if n<0 then
        None
    else
        driver l n

Balanced Trees (Braun Trees)

We would like to implement Braun trees in concoqtion where we can use dependent types to guarantee that the tree is balanced.

Before we begin, let us define a regular tree structure in OCaml

type 'a tree=
| End
| Tree1 of ('a tree)*'a*('a tree)
| Tree2 of ('a tree)*'a*('a tree)
;;

Notice that two cases Tree1 and Tree2 look identical. We intend for Tree1 to represent trees where both branches have the same size while Tree2 is intended for branches of differing sizes. The definition for sized Braun trees is given by

type ('a,'n:'(nat)) braun=
| E : ('a,'(0)) braun
| T1 of let 'm:'(nat) in
    ('a,'(m)) braun*'a*('a,'(m)) braun : ('a,'(S (m*2))) braun
| T2 of let 'm:'(nat) in
    ('a,'(S m)) braun*'a*('a,'(m)) braun : ('a,'(S (S (m*2)))) braun
;;

We can see here how we can enforce our restrictions on the size of each branch. Next, notice that the declared size of each branch is very special. In fact, variations of these sizes such as

'a,'(S (2*m))) braun

will not work. Two see why, we need to recall the definitions of both addition and multiplication in Coq. Addition is defined by

Fixpoint plus (n m:nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (p + m)
  end
where "n + m" := (plus n m) : nat_scope.

In other words

0+m=m
S(p)+m=S(p+m)

Multiplication is defined by

Fixpoint mult (n m:nat) {struct n} : nat :=
  match n with
  | O => 0
  | S p => m + mult p m
  end.

In other words

0*m=0
S(p)*m=m+(p*m)

Returning to our definition, these definitions will allow us to normalize the following

S(S(S(k)*2))
=S(S(2+(k*2)))
=S(S(S(S(0))+(k*2)))
=S(S(S(S(0)+(k*2))))
=S(S(S(S(0+(k*2)))))
=S(S(S(S(k*2))))

Thus, all of our size information will unroll gracefully. This will become extremely important when writing functions based on this definition. Otherwise, we would need to prove a series of lemmas in Coq and then type-cast certain expressions.

Insertion on Braun Trees

First, let us define the insertion function on regular Braun trees

let rec insert (t:'a tree) (x:'a) : 'a tree=
    match t with
    | End  -> Tree1 (End,x,End) 
    | Tree1 (t1,y,t2) ->
        Tree2 ((insert t1 x),y,t2)
    | Tree2 (t1,y,t2) ->
        Tree1 (t1,y,(insert t2 x))
;;

When we add the size information, our functions changes into

let rec binsert .|n:'(nat)| (t:('a,'(n)) braun) (x:'a) : ('a,'(S n)) braun=
    match t in ('a,'(S n)) braun with
    | E  -> T1 .|'(0)| (E,x,E)
    | T1 .|i:'(nat)| (t1,y,t2) ->
        T2 .|'(i)| ((binsert .|'(i)| t1 x),y,t2)
    | T2 .|i:'(nat)| (t1,y,t2) ->
        T1 .|'(S i)| (t1,y,(binsert .|'(i)| t2 x))
;;

This function has type

val binsert :
  (forall n:'(nat) . ('a, '(n)) braun -> 'a -> ('a, '(S n)) braun) = <forall>

Notice that inserting a node is extremely fast since we know apriori whether or not the tree is balanced at a particular junction.

Creating n Copies of an Element

Next, we will define a function to create n copies of a single element. There are many different ways to implement this function. The fastest such algorithms run in log(n) time. A simple implementation in OCaml can be given by

let rec copy x n=
    let rec copy2 x n=
        match n with
        | 0 -> (Tree1 (End,x,End),End)
        | m when m mod 2=1 ->
            let k=(m-1)/2 in
            let (s,t)=copy2 x k in
            (Tree2(s,x,t),Tree1(t,x,t))
        | m when m mod 2=0 ->
            let k=(m-2)/2 in
            let (s,t)=copy2 x k in
            (Tree1(s,x,s),Tree2(s,x,t))
        | _ ->
            raise (BraunErr "Somehow we missed a case in copy2.")
    in
    snd (copy2 x n)
;;

This exploites the special structure of the Braun tree. When ever the number of nodes remaining is odd, we know that both branches will be equal. When the number of nodes remaining is odd, the branches will have a different length. However, since most of the tree is symmetric, we reuse each of these subtrees that we create several times. Implementing this function in Concoqtion is tricky. The problem is that we need to accomplish modular arithmetic on the size of the tree. Although it is possible to write a Coq program to accomplish this in Concoqtion, it is much better to write this as a singleton type. Consider the following definition:

type ('n:'(nat)) eosnat=
| Z : ('(0)) eosnat
| S1 of let 'm:'(nat) in ('(m)) eosnat : ('(S(m*2))) eosnat
| S2 of let 'm:'(nat) in ('(m)) eosnat : ('(S(S(m*2)))) eosnat
;;

This allows us to define the natural numbers in such as way that, in addition, we know whether a number is even or odd. Further, it allows us to unroll our number in such as way that we automatically perform the modular arithmetic needed above. Of course, building these numbers is a bit of a pain, so we need a good driver routine. We define a future that creates these numbers with the following code:

type exists_eosnat=E_eosnat of let 'n:'(nat) in '(n) eosnat
;;

let rec mk_eosnat (n:int) : exists_eosnat =
    match n in exists_eosnat with
    | n when n<=0 -> E_eosnat .|'(0)| Z
    | n when n mod 2=1->
        (match mk_eosnat ((n-1)/2) as exists_eosnat in exists_eosnat with
        | E_eosnat .|n:'(nat)| x->
            E_eosnat .|'(S(n*2))| (S1 .|'(n)| x))
    | n when n mod 2=0->
        (match mk_eosnat ((n-2)/2) as exists_eosnat in exists_eosnat with
        | E_eosnat .|n:'(nat)| x->
            E_eosnat .|'(S(S(n*2)))| (S2 .|'(n)| x))
;;

Notice, we need to use an existential type since we can not verify the size of the resulting number at compile time using a value defined at run time. Also notice that we compute all our modular arithmetic here. Even though we don't need to compute it when we unroll our natural number in the copy function, we have to accomplish this work somewhere. This gives us the tools necessary to define the copy function above. The code is given by:

type ('a) exists_braun=E_braun of let 'n:'(nat) in ('a,'(n)) braun
;;

let bcopy (x:'a) (n:int) : 'a exists_braun =
    match (mk_eosnat n) in 'a exists_braun with
    | E_eosnat .|n:'(nat)| n ->
        let rec copy2 .|n:'(nat)| (x:'a) (n:'(n) eosnat)
            : (('a,'(S n)) braun)*(('a,'(n)) braun)=
            match n as 'n:'(nat) eosnat
                in (('a,'(S n)) braun)*(('a,'(n)) braun) with
            | Z -> (T1 .|'(0)| (E,x,E),E)
            | S1 .|n:'(nat)| n->
                let (s,t)=copy2 .|'(n)| x n in
                (T2 .|'(n)| (s,x,t),T1 .|'(n)| (t,x,t))
            | S2 .|n:'(nat)| n->
                let (s,t)=copy2 .|'(n)| x n in
                (T1 .|'(S n)| (s,x,s),T2 .|'(n)| (s,x,t))
        in
        E_braun .|'(n)| (snd (copy2 .|'(n)| x n))
;;

This illustrates a very important concept when programming in Concoqtion. We transformed this function in order to use structural recursion on a singleton type. This allows us to statically verify all of our size information.

Deleting the Last Inserted Element

Context refinement greatly assists us when writing a routine to remove the last inserted element. The following code removes the element:

let rec bdelete .|n:'(nat)| (t: ('a,'(S n)) braun) : ('a,'(n)) braun =
    match t in ('a,'(n)) braun with
    | T1 .|m:'(nat)| (t1, x, t2) ->
        (match t2 in ('a,'(n)) braun with
        | E -> E
        | T1 .|p:'(nat)| (_, _, _) ->
            T2 .|'(p*2)| (t1, x, bdelete .|'(p*2)| t2)
        | T2 .|p:'(nat)| (_, _, _) ->
            T2 .|'(S (p*2))| (t1, x, bdelete .|'(S (p*2))| t2))
    | T2 .|m:'(nat)| (t1, x, t2) ->
        T1 .|'(m)| (bdelete .|'(m)| t1, x, t2)
;;

Notice, we pass in a tree of size (S n). This prevents us from trying to remove an element from an empty tree. Otherwise, we analyze the tree. When the length of both branches is even, we remove an element from the right subtree. When the length of the left branch is greater, we remove an element from the left branch.

#Interpreter

Writing an Interpreter in Concoqtion

In the next section, we will explore writing an interpreter in Concoqtion. OCaml already provides a very powerful environment to implement interpreters. We can represent the BNF of our language as an OCaml datatype and then recursively loop across its structure. Unfortunately, OCaml does not have the ability to represent typing rules as datatypes. However, we can accomplish this with dependent types. Concoqtion will allow us to implement these structures.

Untyped Lambda Calculus

We can implement an interpreter for untyped lambda calculus with the following OCaml code

type value=
| VInt of int
| VFun of (value -> value)
;;

type exp=
| Int of int
| Val of int
| Lam of exp
| App of exp*exp
;;

exception EvalErr of string;;

let ext env v=
    v::env
;;

let lookup env n=
    List.nth env n
;;

let rec eval e env=
    match e with
    | Int i -> VInt i
    | Val n -> lookup env n
    | Lam e -> VFun (fun v->eval e (ext env v))
    | App (e1,e2) ->
        let v1=eval e1 env in
        let v2=eval e2 env in
        (match v1 with
        | VFun f-> f v2
        | _ -> raise (EvalErr "Tried to evaluate with a nonfunction."))
;;

Two very simply programs are given by

let prog=App (Lam (Val 0),Int 1);;
let prog=App (App (Lam (Lam (Val 0)),Int 1),Int 2);;

Typed Lambda Calculus

We will now develop an interpreter for typed lambda calculus. Normally when we write an interpreter, we pass over the program twice. In the first step, we check that our program is well typed. In the second, we evaluate our program. However, nothing stops us from passing an ill-typed program directly to our evaluation routine. Of course, we would hope that we would never do such a thing, but it is possible. Alternatively, we can develop a notion where all programs passed into the evaluation routines are guaranteed to be well typed. In other words, the parse tree of the program will carry a proof of well-typeness within its own type. Therefore, it is impossible too pass in an ill-typed program into the evaluation routine.

First, we will develop a data structure that we use to represent our programs. This structure is dependently typed and created directly from the typing rules of a well-typed program.

coq
    Inductive type:Set :=
    | Int : type
    | Arrow : type->type->type.

    Inductive env:Set :=
    | Empty : env
    | Ext : env->type->env.
end;;

type ('e:'(env),'t:'(type)) tterm=
| Var0 of let 't:'(type) 'e:'(env) in unit : ('(Ext e t),'(t)) tterm
| VarS of let 't1:'(type) 't2:'(type) 'e:'(env) in ('(e),'(t1)) tterm
    : ('(Ext e t2),'(t1)) tterm
| Abs of let 't1:'(type) 't2:'(type) 'e:'(env) in ('(Ext e t1),'(t2)) tterm
    : ('(e),'(Arrow t1 t2)) tterm
| App of let 't1:'(type) 't2:'(type) 'e:'(env)
    in ('(e),'(Arrow t1 t2)) tterm * ('(e),'(t1)) tterm
    : ('(e),'(t2)) tterm
| Int of let 'e:'(env) in int : ('(e),'(Int)) tterm
;;

As a simple example, let us define the program (lambda x.x)(1) in several different pieces. This will allow us to see how the type of each program carries the proof of well-typeness

let exp1=Var0 .|'(Int),'(Empty)| ();;
let exp2=Abs .|'(Int), '(Int), '(Empty)| exp1;;
let exp3=Int .|'(Empty)| 1;;
let exp4=App .|'(Int), '(Int), '(Empty)| (exp2,exp3);;
let exp=App .|'(Int), '(Int), '(Empty)| (Abs .|'(Int), '(Int), '(Empty)| (Var0 .|'(Int),'(Empty)| ()),Int .|'(Empty)| 1);;

Next, we need to determine the return type of the evaluation function. Here we have two options. In one case, we could develop a new OCaml type called value where we enumerate each possibility. The drawback of this approach is performance. When we want to use these return values, we have to use a match statement to break apart each case. It also seems wasteful since we already know the return type for any program; it is contained within the type of the program itself. Since this type is contained within coq, we need to define a coq function that transforms this type into a valid OCaml type.

coq
    Fixpoint evalT (t:type) : OCamlType :=
    match t with
    | Int => OCaml_int
    | Arrow dom cod => OCaml_Arr (evalT dom) (evalT cod)
    end.

    Fixpoint evalE (e:env) : OCamlType :=
    match e with
    | Empty => OCaml_unit
    | Ext e t => OCaml_Tuple (OCaml_List_cons (evalT t)
        (OCaml_List_cons (evalE e) OCaml_List_nil))
    end.
end;;

Now, we have all of the pieces to create an evaluation function

let rec eval .|e:'(env),t:'(type)| (exp:('(e),'(t)) tterm) (env':'(evalE e))
    : '(evalT t) =
    (* For some reason, the following match statement causes problems. 
    match exp as ('e:'(env),'t:'(type)) tterm in '(evalT t) with *)
    match exp  in '(evalT t) with
    | Var0 .|t:'(type),e:'(env)| _ ->
        fst env'
    (* Note, we coould not reuse e.  We used e1.  Why?? *)
    | VarS .|t1:'(type), t2:'(type), e1:'(env)| x->
        eval .|'(e1), '(t1)| x (snd env')
    | Abs .|t1:'(type), t2:'(type), e:'(env)| body->
        (fun x->eval .|'(Ext e t1), '(t2)| body (x,env'))
    | App .|t1:'(type), t2:'(type), e:'(env)| (rator,rand)->
        (eval .|'(e),'(Arrow t1 t2)| rator env')
            (eval .|'(e), '(t1)| rand env')
    | Int .|e:'(env)| i-> i
;;

This function has type

val eval :
  (forall e:'(env) , t:'(type) .
      ('(e), '(t)) tterm ->
      '((fix evalE (e0 : env) : OCamlType :=
           match e0 with
           | Empty => OCaml_unit
           | Ext e1 t0 =>
               OCaml_Tuple
                 (OCaml_List_cons (evalT t0)
                    (OCaml_List_cons (evalE e1) OCaml_List_nil))
           end) e) ->
      '(evalT t)) =
  <forall>

When we evaluate our programs from above, we receive the following

eval .|'(Ext Empty Int),'(Int)| exp1 (1,());;
- : '(evalT Int) = 1

eval .|'(Empty),'(Arrow Int Int)| exp2 ();;
- : '(evalT (Arrow Int Int)) = <fun>

eval .|'(Empty),'(Int)| exp3 ();;
- : '(evalT Int) = 1

eval .|'(Empty),'(Int)| exp4 ();;
- : '(evalT Int) = 1

eval .|'(Empty), '(Int)| exp ();;
- : '(evalT Int) = 1

Further, we can see that we can return actual OCaml functions from our routine with the following example

# let f=eval .|'(Empty),'(Arrow Int Int)| exp2 ();;
val f : int -> int = <fun>
# f 3;;
- : int = 3

#Bugs

Bugs in Concoqtion

There's a problem with context refinement in the following piece of code from the typed lambda calculus above. If we instead use the following eval function

let rec eval .|e:'(env),t:'(type)| (exp:('(e),'(t)) tterm) (env':'(evalE e))
    : '(evalT t) =
    (* For some reason, the following match statement causes problems. *)
    match exp as ('e:'(env),'t:'(type)) tterm in '(evalT t) with 
    (*match exp  in '(evalT t) with*)
    | Var0 .|t:'(type),e:'(env)| _ ->
        fst env'
    (* Note, we coould not reuse e.  We used e1.  Why?? *)
    | VarS .|t1:'(type), t2:'(type), e1:'(env)| x->
        eval .|'(e1), '(t1)| x (snd env')
    | Abs .|t1:'(type), t2:'(type), e:'(env)| body->
        (fun x->eval .|'(Ext e t1), '(t2)| body (x,env'))
    | App .|t1:'(type), t2:'(type), e:'(env)| (rator,rand)->
        (eval .|'(e),'(Arrow t1 t2)| rator env')
            (eval .|'(e), '(t1)| rand env')
    | Int .|e:'(env)| i-> i 
;;

We receive the following error

File "interp.ml", line 50, characters 6-10:
This expression has type
  '((fix evalE (e : env) : OCamlType :=
       match e with
       | Empty => OCaml_unit
       | Ext e0 t =>
           OCaml_Tuple
             (OCaml_List_cons (evalT t)
                (OCaml_List_cons (evalE e0) OCaml_List_nil))
       end) _UNBOUND_REL_6)
but is here used with type 'a * 'b

Line 50 contains the statement

fst env'

Next, there's also a problem with not using unique names. If we instead define the eval function as

let rec eval .|e:'(env),t:'(type)| (exp:('(e),'(t)) tterm) (env':'(evalE e))
    : '(evalT t) =
    (* For some reason, the following match statement causes problems. 
    match exp as ('e:'(env),'t:'(type)) tterm in '(evalT t) with *)
    match exp  in '(evalT t) with
    | Var0 .|t:'(type),e:'(env)| _ ->
        fst env'
    (* Note, we coould not reuse e.  We used e1.  Why?? *)
    | VarS .|t1:'(type), t2:'(type), e:'(env)| x->
        eval .|'(e), '(t1)| x (snd env')
    | Abs .|t1:'(type), t2:'(type), e:'(env)| body->
        (fun x->eval .|'(Ext e t1), '(t2)| body (x,env'))
    | App .|t1:'(type), t2:'(type), e:'(env)| (rator,rand)->
        (eval .|'(e),'(Arrow t1 t2)| rator env')
            (eval .|'(e), '(t1)| rand env')
    | Int .|e:'(env)| i-> i 
;;

we receive the error

File "interp.ml", line 53, characters 26-27:
Error while checking body of the context-refined branch:
  (e : env) (t2 : type) (t1 : type) (e := Ext e t2 : env) (t := t1 : type)
  This expression has type ('(_UNBOUND_REL_5), '(_UNBOUND_REL_3)) tterm
  but is here used with type ('(_UNBOUND_REL_2), '(_UNBOUND_REL_3)) tterm

Line 53 contains the statement

eval .|'(e), '(t1)| x (snd env')

In one of Angela's programs, there's a strange behavior. The following program works fine:

coq
   Inductive ty: Set :=
   | Int: ty
   | Fun: ty -> ty -> ty.

   Inductive ev: Set :=
   | Empty: ev
   | Ext: ev -> ty -> ev.

   Fixpoint evalT (t:ty): OCamlType :=
     match t with
   | Int => OCaml_int
   | Fun dom cod => OCaml_Arr (evalT dom) (evalT cod)
     end.

   Notation "A -*- B" :=
     (OCaml_Tuple (OCaml_List_cons A (OCaml_List_cons B OCaml_List_nil))) (at level 31, left associativity).
end;;

coq
   Fixpoint evalEnv (e:ev) : OCamlType :=
     match e with
   | Empty => OCaml_unit
   | Ext env t => (evalEnv env) -*- (evalT t) end.
end;;

Yet this program

coq
   Inductive ty: Set :=
   | Int: ty
   | Fun: ty -> ty -> ty.

   Inductive ev: Set :=
   | Empty: ev
   | Ext: ev -> ty -> ev.

   Fixpoint evalT (t:ty): OCamlType :=
     match t with
   | Int => OCaml_int
   | Fun dom cod => OCaml_Arr (evalT dom) (evalT cod)
     end.

   Notation "A -*- B" :=
     (OCaml_Tuple (OCaml_List_cons A (OCaml_List_cons B OCaml_List_nil))) (at level 31, left associativity).

   Fixpoint evalEnv (e:ev) : OCamlType :=
     match e with
   | Empty => OCaml_unit
   | Ext env t => (evalEnv env) -*- (evalT t) end.
end;;

Fails with error

EXCEPTION:
  At location 509-510:
  Syntax error: [constr:operconstr] expected after '-' (in [constr:operconstr])

The only difference between the two programs is that the first uses two Coq blocks while the second only uses one.

The following program yields an error:

type 'm:'(nat) snat=
| Z: '(0) snat
| S of let 'm:'(nat) in '(m) snat : '(S m) snat
;;

type exists_snat=E_snat of let 'n:'(nat) in '(n) snat    
;;

let mk_snat (n:int) : exists_snat =
    match n as int in exists_snat with
    | n when n<=0 -> E_snat .|'(0)| Z
    | n when n>0 ->
        match mk_snat (n-1) as exists_snat in exists_snat with
        | E_snat .|n:'(nat)| my_snat->
            E_snat .|'(1+n)| (S .|'(n)| my_snat)
;;  

EXCEPTION:
  Anomaly: assert failure
  (file "parsing/printast.ml", line 1509, characters 6-12). Please report.

This program yields a valid error (mk_snat not defined) when the guard statements "when" are removed.

-- JosephYoung - 31 Jan 2007

End of topic
Skip to actions | Back to top