Support type annotations #84

Open
xrchz opened this Issue Oct 5, 2015 · 9 comments

Projects

None yet

3 participants

@xrchz
Member
xrchz commented Oct 5, 2015

Would be nice to add this feature to CakeML. Also see this thread for further motivation https://lists.cakeml.org/pipermail/users/2015-October/000066.html

@SOwens SOwens was assigned by xrchz Oct 5, 2015
@tanyongkiam
Contributor

It might be worth taking a closer look at the module system in general:

This does not type check either:

structure foo :> sig val x : int end = struct val x = 5 end;

(I think probably because undoing of type abbreviations is incorrectly applied / missing somewhere)

@xrchz
Member
xrchz commented Nov 11, 2015

probably something like this to fix the above bug (untested)

diff --git a/semantics/typeSystem.lem b/semantics/typeSystem.lem
index 049a44e..841a31b 100644
--- a/semantics/typeSystem.lem
+++ b/semantics/typeSystem.lem
@@ -723,7 +723,7 @@ sval : forall mn tenvT x t specs flat_tenvT cenv tenv fvs decls.
 check_freevars 0 fvs t &&
 type_specs mn tenvT specs decls flat_tenvT cenv tenv
 ==>
-type_specs mn tenvT (Sval x t :: specs) decls flat_tenvT cenv (tenv++[(x,(List.length fvs, type_subst (alistToFmap (List_extra.zipSameLength fvs (List.map Tvar_db (genlist (fun x -> x) (List.length fvs))))) t))])
+type_specs mn tenvT (Sval x t :: specs) decls flat_tenvT cenv (tenv++[(x,(List.length fvs, type_subst (alistToFmap (List_extra.zipSameLength fvs (List.map Tvar_db (genlist (fun x -> x) (List.length fvs))))) (type_name_subst tenvT t)))])

 and
@xrchz xrchz added a commit that referenced this issue Nov 11, 2015
@xrchz xrchz start refactoring type system environment into a record
replace tenvM/C/E/T with a type_environment record

also included a potential fix to the bug mentioned in #84

proofs not updated
a2d0931
@xrchz
Member
xrchz commented Nov 12, 2015

The problem mentioned above is possible more serious, and not to do with type abbreviations at all:

structure foo = struct val x = 5 end;
<type error>

EDIT: oops, I just realised this is because I was trying to redefine an existing structure.

@xrchz
Member
xrchz commented Nov 12, 2015

The attempted fix above, using type_name_subst, appears not to work.
EDIT: ugh, actually, it seems like I hadn't run lem to update the Script file, so the change remains untested...

@tanyongkiam
Contributor

That example runs fine on my version of the REPL and also the explorer
(which I assume got updated).

Did it occur after you added type_name_subst?

On Thu, Nov 12, 2015 at 5:38 PM, Ramana Kumar notifications@github.com
wrote:

The attempted fix above, using type_name_subst, appears not to work.


Reply to this email directly or view it on GitHub
#84 (comment).

@xrchz
Member
xrchz commented Nov 12, 2015

Sorry: that was a false alarm - I had defined foo twice in one session. I am now rebuilding things in order to test whether type_name_subst works for the original example. (The explorer won't be updated until that works.)

@xrchz
Member
xrchz commented Nov 12, 2015

Scott and I are thinking of leaving this broken on version1, and just fixing it on master, since it looks like it might have various knock-on effects on the type soundness and inferencer proofs.

@SOwens SOwens added a commit that referenced this issue Nov 13, 2015
@SOwens SOwens Finish refactoring fixes
There is a cheat due to a proof not being updated for a real change in
the semantics related to #84
af53bfe
@xrchz xrchz added a commit that referenced this issue Nov 13, 2015
@xrchz xrchz weaken type_specs_tenv_ok slightly, and prove cheat in it
also add additional assumption to the type_specs rule for sval.
this is related to the example in #84.
3fd45db
@xrchz
Member
xrchz commented Jul 27, 2016

@SOwens what is the status of this? I think I've seen a lot of work towards it recently.

@SOwens
Member
SOwens commented Jul 27, 2016

@theolaurent has been working on it. The inferencer completeness proof needs updating, as does the source_to_mod poof (but that should be trivial).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment