Zulip Chat Archive

Stream: general

Topic: Type Reflection in Lean


view this post on Zulip Alcides Fonseca (Mar 11 2021 at 08:59):

inductive WOptions
| A
| B

attribute [derive decidable_eq] WOptions

inductive Wrapper: WOptions  Type
| W {w} : Wrapper w

open Wrapper

attribute [derive decidable_eq] Wrapper

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T := if h:T=U then u else t

I wrote this MVE that does not work in the dite. I derived decidable_eq to remove the issue of deciding whether T could be U. My goal (in a bigger project) is to do type-safe substitution on a strongly-typed AST. Is this simply not possible?

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:40):

Do you have a sketch for your bigger example? For the general pattern of this if-then, where you check if the indices match and then use a subst, it's usually easiest to work with function.update, but I suspect an #xy problem here

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:43):

In this case

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T :=
if h:T=U then by rw h; exact u else t

works

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:45):

It's also not clear to me in what way this is supposed to represent "type reflection" as in your title

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:45):

the Wrapper types are all singletons so they don't carry any information

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:46):

the function f is thus provably equal to

def f {T U : WOptions} (t:Wrapper T) (u:Wrapper U) : Wrapper T := ⟨⟩

view this post on Zulip Mario Carneiro (Mar 11 2021 at 09:46):

although that's probably a side effect of minimization

view this post on Zulip Alcides Fonseca (Mar 11 2021 at 10:36):

Thanks, it worked. Somehow I was missing the exact tactic (thinking after the ; I was back in term mode).

view this post on Zulip Alcides Fonseca (Mar 11 2021 at 11:12):

This is the full (relevant) code:

@[derive decidable_eq]
inductive TType
| TBool : TType
| TNat : TType
| Fun : TType  TType  TType

open TType

@[reducible]
def context := list (string × TType)

def keys (Γ: context) : list string := list.map (λ x, prod.fst x) Γ

inductive Term : TType  Type
| LiteralNat :   Term TNat
| LiteralBool : bool  Term TBool
| Var {Γ: context} {T} (x: string) (p: (x, T)  Γ) : Term T
| Abs {Γ: context} {U} (x:string) (T: TType) (e:Term U) (p: x  keys(Γ)) : Term (Fun T U)
| App {T U} (t1: Term (Fun T U)) (t2: Term T) : Term U
| Ite {T} (t1:Term TBool) (t2 t3 : Term T) : Term T

open Term

def substitution {T U} (t: Term T) (n: Term U) (x: string) : Term T :=
  match (t:Term T) with
   | (Var name p) := if h:T = U then by rw h; exact n else t
   -- | (LiteralBool b) := LiteralBool b
   | _ := t
  end

I am troubling getting the interaction between the T and the pattern matching. I knew that using dite, I could apply some tactic to solve it (although the syntax was a mystery to me). But using match, the second (comment) pattern does not work, because it cannot understand that it should only cover when T = TBool.
And even though I have a catch-all wildcard, it complains that I do not cover all the cases.

view this post on Zulip Mario Carneiro (Mar 11 2021 at 15:49):

There appears to be an issue in getting the wildcard case to typecheck, that prevents the wildcard from working correctly without some kind of untypechecked macro expansion. Here's a version that works, which is what the wildcard compiles to anyway:

def substitution {T U} (t: Term T) (n: Term U) (x: string) : Term T :=
match T, t with
| T, t@(Var name p) := if h:T = U then by rw h; exact n else t
| _, t@(LiteralNat _) := t
| _, t@(LiteralBool _) := t
| _, t@(Abs _ _ _ _) := t
| _, t@(App _ _) := t
| _, t@(Ite _ _ _) := t
end

view this post on Zulip Mario Carneiro (Mar 11 2021 at 15:50):

Note that it is necessary to simultaneously match on T and t, because Term is an inductive type with the TType as an index (it's an inductive family), so it has to be able to vary in recursions

view this post on Zulip Mario Carneiro (Mar 11 2021 at 15:51):

By the way, the definition of Term is incorrect, since the contexts used in the Var and Abs constructors are not constrained to relate to anything else. The context should be another index to the inductive type

view this post on Zulip Mario Carneiro (Mar 11 2021 at 15:54):

like this:

inductive Term : context  TType  Type
| LiteralNat {Γ} :   Term Γ TNat
| LiteralBool {Γ} : bool  Term Γ TBool
| Var {Γ T} (x: string) (p: (x, T)  Γ) : Term Γ T
| Abs {Γ U} (x:string) (T: TType) (e:Term ((x,T)::Γ) U) (p: x  keys(Γ)) : Term Γ (Fun T U)
| App {Γ T U} (t1: Term Γ (Fun T U)) (t2: Term Γ T) : Term Γ U
| Ite {Γ T} (t1:Term Γ TBool) (t2 t3 : Term Γ T) : Term Γ T

open Term

def substitution {Γ T U} (x: string) (t: Term ((x, U)::Γ) T) (n: Term Γ U) : Term Γ T :=
sorry

view this post on Zulip Alcides Fonseca (Mar 11 2021 at 16:06):

Yes, you are correct in the Term definition. I was actually simplifying it to try and spot the issue on the match.
I was missing the simultaneous matching. That seems to be the key.
Thank you so much again!

view this post on Zulip Mario Carneiro (Mar 11 2021 at 16:26):

Here's a setup that I believe to be provable:

def context := alist (λ _: string, TType)

def keys : context  list string := alist.keys

instance : has_mem (string × TType) context := λ x, T Γ, T  Γ.lookup x

def cons (Γ : context) (x:string) (T:TType) (h : x  Γ.keys) : context :=
⟨⟨x,T⟩::Γ.1, list.nodupkeys_cons.2 h, Γ.2⟩⟩

inductive Term : context  TType  Type
| LiteralNat {Γ} :   Term Γ TNat
| LiteralBool {Γ} : bool  Term Γ TBool
| Var {Γ : context} {T} (x: string) (p: (x, T)  Γ) : Term Γ T
| Abs {Γ U} (x:string) (T: TType) (p: x  keys Γ) (e:Term (cons Γ x T p) U) : Term Γ (Fun T U)
| App {Γ T U} (t1: Term Γ (Fun T U)) (t2: Term Γ T) : Term Γ U
| Ite {Γ T} (t1:Term Γ TBool) (t2 t3 : Term Γ T) : Term Γ T

open Term

def substitution_aux {Γ U} (x : string) (n : Term Γ U) :
   {Γ' T}, Term Γ' T  Γ'.1 ~ x, U⟩::Γ.1  Term Γ T
| Γ' _ (LiteralNat n) hp := LiteralNat n
| Γ' _ (LiteralBool b) hp := LiteralBool b
| Γ' U' (Var name p) hp :=
  begin
    have other : Term Γ U' := Var name _,
    { exact if name = x then if h : U' = U then by rw h; exact n else other else other },
    sorry
  end
| Γ' _ (@Abs _ U' y T' p e) hp := sorry
| Γ' U' (@App _ T' _ t1 t2) hp := sorry
| Γ' T' (Ite t1 t2 t3) hp := sorry

def substitution {Γ T U} (x: string) (p) (t: Term (cons Γ x U p) T) (n: Term Γ U) : Term Γ T :=
substitution_aux x n t (list.perm.refl _)

view this post on Zulip Mario Carneiro (Mar 11 2021 at 16:29):

The point of using alist instead of list here is so that the use of list permutation in the statement of substitution_aux doesn't change the types of existing variables. This is needed in order to commute the cons application in the type of substitution with the one in the type of Abs

view this post on Zulip Mario Carneiro (Mar 11 2021 at 16:30):

You can also avoid the use of permutation entirely if you use finmap instead of alist, since that bakes the permutations into the type

view this post on Zulip Mario Carneiro (Mar 11 2021 at 16:31):

Alternatively, you can stick with list and use the more precise context Γ ++ (x,U) :: Δ in the type of substitution

view this post on Zulip Alcides Fonseca (Mar 22 2021 at 19:08):

(Sorry for the late reply, had a couple of deadlines)
Thank you very much for the reply! It helped much more than just answering the question. I'll have to buy you a drink next time I'll visit CMU (if you are still there)

view this post on Zulip Alcides Fonseca (Mar 22 2021 at 19:32):

A follow-up issue: I want to show that a set of term synthesis rules (like the opposite of type-checking). However, using a strongly-typed AST breaks the way I was stating the synthesis rules. I have simplified the problem to this exame, where the language has OptionA and OptionB, with the type indexed by a number (in the larger example it is the context and type). I want to state that I can generate one of each, and then show completeness of the generation (which will not work in this case, unless I add that n < 2)

inductive term :   Type
| optionA : term 0
| optionB : term 1


inductive synth {n:} : term n  Prop
| generateOptionA : synth (term.optionA)
| generateOptionB : synth (term.optionB)


theorem completeness {n:} :  (t:term n), synth n t := by sorry

Lines generateOptionA and B do not compile:

type mismatch at application
  synth term.optionA
term
  term.optionA
has type
  term 0
but is expected to have type
  term n

How can I refined the type to use index 0? I have tried to make n:\Nat explicit, but it did not work.

view this post on Zulip Mario Carneiro (Mar 22 2021 at 21:49):

Actually you don't need n < 2 for this proof

view this post on Zulip Mario Carneiro (Mar 22 2021 at 21:50):

inductive term :   Type
| optionA : term 0
| optionB : term 1

inductive synth :  {n:}, term n  Prop
| generateOptionA : synth term.optionA
| generateOptionB : synth term.optionB

theorem completeness :  {n:} (t:term n), synth t
| _ term.optionA := synth.generateOptionA
| _ term.optionB := synth.generateOptionB

Last updated: May 13 2021 at 00:41 UTC