using equality hypothesis in type inference

Stream: new members

[Kris Brown]

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]

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]

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]

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

[Kenny Lau]

this is what we call dependent equality hell

[Mario Carneiro]

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]

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]

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]

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]

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]

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).