~thon/thon

99dcfcf68615e2bddf807faf002d83501449e244 — Evan Bergeron 6 months ago 49cadea
Push use type variable name in setDeBruijinInType; flesh out example
3 files changed, 31 insertions(+), 12 deletions(-)

M README.md
M examples/setget.thon
M thon.sml
M README.md => README.md +16 -3
@@ 140,13 140,26 @@ Both of these expression have type `((nat -> T) * (T -> nat))` for
some type `T`. Note this is an existential claim, hence the name
existential packages.

These implementations can be used interchangably by saying
An implementation can be used as follows:

```
use (...either implementation...) as (pkg, t) in
(... some use of pkg ...)
let setget : some t. ((nat -> t) * (t -> nat)) =
    (impl some t. ((nat -> t) * (t -> nat)) with nat as
    (
        ((*set*) \ x : nat -> x,
        (*get*) \ x : nat -> x)
     ))
in use setget as (sg, t) in
let set : (nat -> t) = fst sg in
let get : (t -> nat) = snd sg in
let s : t = set (S S Z) in
let g : nat = get s in
g
```

Note that since the type variable `t` declared in the `use` clause is
abstract, we can equivalently use the other implementation.

## recursive types

`data nats = (unit | (nat * nats))` is the type of lists natural numbers. 

M examples/setget.thon => examples/setget.thon +12 -5
@@ 1,5 1,12 @@
impl some t. ((nat -> t) * (t -> nat)) with nat as
(
    ((*set*) \ x : nat -> x,
    (*get*) \ x : nat -> x)
)
let setget : some t. ((nat -> t) * (t -> nat)) =
    (impl some t. ((nat -> t) * (t -> nat)) with nat as
    (
        ((*set*) \ x : nat -> x,
        (*get*) \ x : nat -> x)
     ))
in use setget as (sg, t) in
let set : (nat -> t) = fst sg in
let get : (t -> nat) = snd sg in
let s : t = set (S S Z) in
let g : nat = get s in
g

M thon.sml => thon.sml +3 -4
@@ 162,7 162,7 @@ fun substTypeInExp' srcType dstExp bindingDepth =
            A.Use(substTypeInExp' srcType pkg bindingDepth,
                  clientName,
                  typeName,
                  substTypeInExp' srcType client (bindingDepth+1)) (*inds type var*)
                  substTypeInExp' srcType client (bindingDepth+1)) (*binds type var*)
       | A.Fold(t, e') => A.Fold(substType' srcType t bindingDepth,
                             substTypeInExp' srcType e' (bindingDepth+1)) (* binds typ var *)
       | A.Unfold(e') => A.Unfold(substTypeInExp' srcType e' bindingDepth)


@@ 256,7 256,7 @@ fun setDeBruijnIndex e varnames typnames =
            setDeBruijnIndex pkg varnames typnames,
            clientName,
            typeName,
            setDeBruijnIndex client (clientName::varnames) typnames) (* TODO need a type name still *)
            setDeBruijnIndex client (clientName::varnames) (typeName::typnames))
       | A.TypApp (appType, e) =>
            A.TypApp (setDeBruijnIndexInType appType varnames typnames,
                      setDeBruijnIndex e varnames typnames)


@@ 1078,8 1078,7 @@ val zerobst = parseFile "/home/evan/thon/examples/singletonbst.thon";
val appbst = eval (A.App(A.App(bstinsert, A.Zero), emptybst));
val true = (zerobst = appbst);

val setget = parseFile "/home/evan/thon/examples/setget.thon";
val Some ("t",Prod (Arr (Nat,TypVar ("t",0)),Arr (TypVar ("t",0),Nat))) = typeof setget;
val Succ (Succ Zero) = runFile "/home/evan/thon/examples/setget.thon";

in
()