Constrain function input to one constructor

Stream: lean4

[Yuri de Wit]

Say I have the following inductive type:

inductive Term where
  | Var (name : String)
  | Dup (nam0 : String) (name1 : String) (expr : Term) (body : Term)
  | Let (name : String) (expr : Term) (body : Term)
  | Lam (name : String) (body : Term)
  | App (func : Term) (argm : Term)
  | Ctr (name : String) (args: List Term)
  | U32 (numb : UInt64)
  | Op2 (oper : Operation) (val0 : Term) (val1 : Term)

I would like to define a function that only accepts Ctr terms as an input.

I know this can be done with something like:

def flatten : Rule -> Rule
| Ctr name args => sorry
| _ => fatal! ...

But instead of handling this in the function at runtime, I would like to make sure this function is never called with anything other than with a Ctr. Is there a way to achieve that at compile time?

The first thing that comes to mind is to use a phantom type to discriminate the cases I am interested, but I am wondering if there are other ways.

[Yuri de Wit]

I also understand that depending on the application, this may just shift the burden of pattern matching to the client and that may be counter productive.

[Yuri de Wit]

In my case, I believe this question is coming from the fact that the left-hand-side of Rule can only be a constructor in:

structure Rule where
  lhs : Term
  rhs : Term

Maybe lhs should be a separate type.

[Simon Hudon]

A typical piece of advice here is to accept that flatten can be called on arbitrary expressions and write your theorems with the side condition that the term is a Ctr.

You can also create a Type just for representing a Ctr and provide functions Term -> Option Ctr and Ctr -> Term. Then you can make flatten take a Ctr as a parameter.

[Horatiu Cheval]

The function flatten seems to have type Term -> Term in this example? In any case, you could define a predicate isCtr only satisfied by those Term which are applications of Ctr, and require a proof of that in the type of flatten. (Is this what you mean by a phantom type?)

[Yuri de Wit]

Horatiu Cheval said:

The function flatten seems to have type Term -> Term in this example?

Sorry, I tried to simplify the example and made it incorrect.

The real flatten function takes a List Rule and needs to group them by LHS Ctr name (note this is a work in progress and does not compile ...)

abbrev RuleGroup := Std.HashMap String (Array Rule)

def groupBy (rules: List Rule) : RuleGroup :=
  return rules.foldl groupByName Inhabited.default
  where
    groupByName : RuleGroup -> Rule -> RuleGroup
    | rg, ⟨ (Term.Ctr name args), rhs ⟩ => match rg.find? name with
              | none    => rg.insert name [rule]
              | some rs => rs.push rule

(btw, it turns out List.groupBy has an unexpected type/impl to me, at least)

[Yuri de Wit]

Horatiu Cheval said:

(Is this what you mean by a phantom type?)

I mean something along the lines of (does not compile):

inductive IsCtr where
  | yes
  | no

inductive Term (a : IsCtr) where
  ...
  | Ctr (name : String) (args: List a) : Term IsCtr.yes

So that I could, for instance:

def test : Term IsCtr.yes -> Term

[Yuri de Wit]

Simon Hudon said:

A typical piece of advice here is to accept that flatten can be called on arbitrary expressions and write your theorems with the side condition that the term is a Ctr.

Could you provide a simple example of how this could be done?

[Simon Hudon]

Your definition with panic! is the definition I was thinking of. For a theorem, I'd need an example of the kind of theorem you're working on

[Simon Hudon]

If you're trying to statically know which constructor you're working with, you can also go this way:

inductive Term where
  | Var (name : String)
  | Lam (name : String) (body : Term)
  | App (func : Term) (argm : Term)
  | Ctr (name : String) (args: List Term)

inductive TermCase where
  | Var
  | Lam
  | App
  | Ctr
open Term

inductive IsTermCase : Term → TermCase → Prop where
  | Var : IsTermCase (Var v) TermCase.Var
  | Lam : IsTermCase (Lam v t) TermCase.Lam
  | App : IsTermCase (App t₀ t₁) TermCase.App
  | Ctr : IsTermCase (Ctr c ls) TermCase.Ctr

def SpecificTerm (c : TermCase) := { t // IsTermCase t c }

def Term.check : Term → Option (SpecificTerm c) := sorry
def Term.ofSpecific : SpecificTerm c → Term := Subtype.val

def useVar : SpecificTerm TermCase.Var → Nat := sorry

def specialize (t : Term) (h : IsTermCase t c := by constructor) :
    SpecificTerm c :=
⟨t, h⟩

def useVar? : Term → Option Nat
| Var v => some <| useVar (specialize (Var v))
| _ => none

def varName : SpecificTerm TermCase.Var → String
| ⟨ Var s, _ ⟩ => s

useVar? shows how easy it is (using specialize) to create a SpecificTerm when you have local information about which constructor you're faced with. varName shows you can the equation compiler can dismiss all the impossible cases.

[Simon Hudon]

The boilerplate seems easy enough to generate automatically.

[Simon Hudon]

The design can also work by replacing IsTermCase with a function Term -> TermCase and that can make it easier to derive a Decidable instance for the corresponding propositions, if that matters

[Chris B]

In the past I've used this:

def flatten (r : Rule) (h : ∃ name args, r = Ctr name args := by decide) : Rule := ...

You'll have to write the decidable instance, but with the optional/auto arg by decide, you can usually pretend it's not there. If you use it a lot you can extract the existential hypothesis into a predicate isCtr or whatever.

[Simon Hudon]

The downside of not wrapping that proof into a subtype @Chris B is that now, when writing a theorem about flatten, you have proof term floating around making rewriting more awkward. By moving that proof term to a function that done nothing but wrap the subtype, you can write separate theorems about the wrapping and the flatten function.

[Simon Hudon]

This formulation for h also seems hard to use by the equation compiler when trying to find unreachable cases

[Chris B]

Touche, I agree that the explicit existential is more ad-hoc. My use case has been just "this function should only work for this constructor" without the need for a lot of subsequent proving.

[Simon Hudon]

That's fair. I think we can generalize both approaches btw. For generally decidable predicates, we can define decidable subtypes:

variable {T : Type} {p : T → Bool}

def DecSubtype (p : T → Bool) := { t // p t = true }

def Term.caseOf : Term → TermCase
| Var s => TermCase.Var
| App _ _ => TermCase.App
| Lam _ _ => TermCase.Lam
| Ctr _ _ => TermCase.Ctr

def VarTerm :=
DecSubtype (λ t => decide <| Term.caseOf t = TermCase.Var)

def VarOrLamTerm :=
DecSubtype (λ t => decide <| Term.caseOf t = TermCase.Var ∨ Term.caseOf t = TermCase.Lam)

def specialize (t : T) (h : p t = true := by rfl) :
    DecSubtype p :=
⟨t, h⟩

def varName : VarTerm → String
| ⟨ Var s, _ ⟩ => s

def boundVarName : VarOrLamTerm → String
| ⟨ Var s, _ ⟩ => s
| ⟨ Lam s _, _ ⟩ => s

[Simon Hudon]

(This is a really cool problem btw. Thanks @Yuri de Wit! You've convinced me I want that in my library)

[Yuri de Wit]

Simon Hudon said:

(This is a really cool problem btw. Thanks Yuri de Wit! You've convinced me I want that in my library)

I am glad my ignorance was useful! Now I need to digest all this!

[Mario Carneiro]

No one mentioned the simplest solution, which is to not accept Term at all and instead pass arguments (name : String) (args: List Term) to the function

[Mario Carneiro]

it's kind of an #xy solution but it is usually easier to use than the other suggestions

[Yuri de Wit]

True, except that the real flatten (my fault, since I did not provided it in its full glory) is def flatten : List Rule -> RuleGroup (RuleGroup is an HashMap String (Array Rule)).

So I need to process a list of Rules (structure Rule (lhs: Term) (rhs: Term)) containing Term's, instead of a single Term.

[Yuri de Wit]

Another solution would be to simply create a dedicated type for the left hand side at the expense of some duplication of the Ctr definition, as far as I can see.

[Mario Carneiro]

If you are just writing lean 4 code and are not fussed about proofs, you can just use if let and skip the elements that are not of the required form

[Mario Carneiro]

or panic! if you find them