## Stream: new members

### Topic: using equality hypothesis in type inference

#### Kris Brown (Jul 11 2020 at 05:58):

I'm modeling a program execution, with a list of named variables of different types. Below is an almost-working MWE:

@[derive decidable_eq]
inductive datatype
| is_nat : datatype
| is_bool : datatype

open datatype

def dt_map : datatype -> Type
| is_nat  := nat
| is_bool := bool

def variable_list := list (string × (Σ dt: datatype, dt_map dt))

def examplelist : variable_list := [("b", ⟨is_bool, tt⟩),
("i", ⟨is_nat,  (0:ℕ)⟩),
("j", ⟨is_nat,  (3:ℕ)⟩)]

def get_variable: Π{t_key: datatype},
string → variable_list → option (dt_map t_key)
| _ _ nil := none
| dtype key ((key', ⟨dtype', val⟩) :: t) :=
if hyp : key = key' ∧ dtype=dtype'
then some val   -- ERROR, has type (dt_map dtype') expected (dt_map dtype)
else @get_variable dtype key t


The issue is that type inference doesn't know that two things are equal (which are certainly equal, by hypothesis). Is there a way to signal this to Lean (or incorporate a proof that uses hyp)?

#### Kyle Miller (Jul 11 2020 at 06:09):

You have to rewrite the type using the hypothesis somehow. I'm not too good with that in term mode, but this works:

def get_variable: Π{t_key: datatype},
string → variable_list → option (dt_map t_key)
| _ _ [] := none
| dtype key ((key', ⟨dtype', val⟩) :: t) :=
if hyp : key = key' ∧ dtype=dtype'
then begin rw hyp.2, exact some val, end
else @get_variable dtype key t


Note: there was a bug in the first equation, since nil was being interpreted as a variable name rather than the constructor for the empty list.

#### Kyle Miller (Jul 11 2020 at 06:24):

I don't know how idiomatic it is, but you can replace the begin ... end block in that with eq.rec (some val) hyp.2.symm.

#### Kris Brown (Jul 11 2020 at 06:31):

thank you, makes sense! (and thanks for finding that bug)

#### Kenny Lau (Jul 11 2020 at 06:37):

this is what we call dependent equality hell

#### Mario Carneiro (Jul 11 2020 at 08:03):

I would suggest encapsulating the cast into a function like so:

def as_type {dt} (t : dt_map dt) (dt') : option (dt_map dt') :=
if h : dt = dt' then some (by rw ← h; exact t) else none

def get_variable : Π {t_key: datatype}, string → variable_list → option (dt_map t_key)
| _ _ [] := none
| dtype key ((key', ⟨dtype', val⟩) :: t) :=
if key = key' then as_type val _ else @get_variable dtype key t


#### Mario Carneiro (Jul 11 2020 at 08:08):

Alternatively, using alist:

import data.list.alist

@[derive decidable_eq]
inductive datatype
| is_nat : datatype
| is_bool : datatype

open datatype

def dt_map : datatype -> Type
| is_nat  := nat
| is_bool := bool

def variable_list := alist (λ _:string, Σ dt: datatype, dt_map dt)

def examplelist : variable_list :=
list.to_alist [
⟨"b", is_bool, tt⟩,
⟨"i", is_nat, (0:ℕ)⟩,
⟨"j", is_nat, (3:ℕ)⟩]

def as_type {dt} (t : dt_map dt) (dt') : option (dt_map dt') :=
if h : dt = dt' then some (by rw ← h; exact t) else none

def get_variable {t_key: datatype} (key : string) (t : variable_list) : option (dt_map t_key) :=
do ⟨dt, val⟩ ← t.lookup key, as_type val t_key


#### Reid Barton (Jul 11 2020 at 10:48):

Note that Mario's first snippet changes the meaning of the function in the case that the environment contains multiple variables with the same name but different types.

#### Reid Barton (Jul 11 2020 at 10:50):

If you're modeling an untyped language (e.g. Python) then I suspect you would be happier with

inductive value : Type
| mk_nat : nat -> value
| mk_bool : bool -> value


and have an environment mapping variables names to values.

#### Reid Barton (Jul 11 2020 at 10:52):

If you're really modeling a language where name lookup is type-dependent then how about using a separate environment for each type?

#### Kris Brown (Jul 11 2020 at 20:22):

Thanks! I didn't know about alist and it seems perfect for this application.

I'm modeling a strongly/statically typed language (Golang) and basing my initial efforts on this repo (https://github.com/coq-community/hoare-tut/ - haven't found any comparable resource in Lean) which requires the language model to implement the following

  Parameter Var: Type -> Type.
Parameter Expr: Type -> Type.
Parameter Env: Type.
Parameter upd: forall (A:Type), (Var A) -> A -> Env -> Env.
Parameter eval: forall (A:Type), (Expr A) -> Env -> A.


And I'm modifying eval to return option A to allow modeling a compiler error for undefined variable reference. I suspect Mario's snippet has the right behavior for Env in this case (if a program requests a variable by name but is expecting a different type, this should be an error).

Last updated: May 14 2021 at 07:19 UTC