search

vekatze / neut

A functional programming language with static memory management
https://vekatze.github.io/neut/
MIT License
840 stars 11 forks source link

Can construct value from nothing with `case` #10

Closed L-as closed 1 year ago

L-as commented 4 years ago

Example:

(inductive Example ((a tau))
  (new ((x a)) (Example (Π () a))))

(let (ex (Example (Π () i64))) (Example.new i64 0))
(let (f (Π () i64)) (Example.case (Π () i64) (Π () i64) ex (Π-introduction ((f (Π () i64))) f)))

(f)

This results in a SIGSEGV on my machine, for obvious reasons. The issue seems to be the type of Example.case: (Π ((internal.case-tau tau) (a tau) (_ (Example a)) (Example.new (Π ((x a)) internal.case-tau))) internal.case-tau)

The a used when creating ex and the a in the type of ex are confused it seems.

L-as commented 3 years ago

After thinking over this, you ought to separate parameters and indices like is done in other dependently typed languages. Then, the return type of the constructor should only allow you to specify indices. You could even just remove the I p_0 ... p_1 part from the return type, where I is the inductive type and p_i are the parameters. The above code could e.g. become:

(inductive Example () ((_ tau))
  (new ((a tau) (x a)) ((Π () a))))

(let (ex (Example (Π () i64))) (Example.new i64 0))
(let (f (Π () i64)) (Example.case (Π () i64) (Π () i64) ex (λ (a x) x))) ; won't compile

(f)

The case eliminator ceases to be powerful enough though, since you can't unwrap the Example anymore.

Translating the above inductive type to Coq:

Inductive Example : Type -> Type :=
    example_new : forall (A : Type) (x : A), Example A.

Then we get the following eliminator:

Example_rect
     : forall P : forall T : Type, Example T -> Type,
       (forall (A : Type) (x : A), P A (exnew A x)) ->
       forall (T : Type) (e : Example T), P T e

This also allows one to define a function which unwraps the Example, which isn't possible with the primitive case, as evidenced here:

Definition extract (A : Type) (ex : Example A) : A :=
    Example_rect (fun T _ => T) (fun A x => x) A ex.

If you gave Example.case a type like the one for Example_rect, then you could define something like extract in neut too.

Fixing this would also allow you to define a HList in neut, which is currently impossible! I actually came across this bug because I was trying to implement a heterogeneous list in neut.

vekatze commented 1 year ago

Hi, from the future. Thanks for your good catch. Also sorry for my (astronomically) delayed reply. It has been about three years since this issue was opened, and now Neut doesn't have GADTs but only ADTs, at least for now. Because of that, I can't immediately apply your suggested fix, but I'll definitely reflect your point when I chose to re-add GADTs to the language.