Zulip Chat Archive

Stream: new members

Topic: using equality hypothesis in type inference


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kris Brown (Jul 11 2020 at 06:31):

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

view this post on Zulip Kenny Lau (Jul 11 2020 at 06:37):

this is what we call dependent equality hell

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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