# Zulip Chat Archive

## 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 `value`

s.

#### 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: Dec 20 2023 at 11:08 UTC