Create row types for PHOAS

Stream: lean4

[Anders Christiansen Sørby]

I'm trying to create a language parser and type checker with row types. Like a JSON type I need to have a recursive definition. I tried building on the PHOAS tutorial in the Lean4 manual.

This is my naive attempt at defining a PHOAS with the row types Attrset

mutual
/-- Attribute set type this is supposed to be able to represent every available type
-/
inductive AttrsetTy
  | empty
  | merged (n : Name) (v : Ty) (a : AttrsetTy)


/-- Primitive types
-/
inductive Ty where
  | num
  | string
  | bool
  | lambda : Ty -> Ty -> Ty
  -- Optimized primitives
  | list : Ty -> Ty
  | attrset : AttrsetTy → Ty
end
/--
Hetrogenous list of types paramtereized by ɑ
-/
inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β i → HList β is → HList β (i::is)

infix:67 " :: " => HList.cons

notation "[" "]" => HList.nil


/-- Member certificate for list elements
-/
inductive Member : α → List α → Type
  | head : Member a (a::as)
  | tail : Member a bs → Member a (b::bs)

def HList.get : HList β is → Member i is → β i
  | a::as, .head => a
  | _::as, .tail h => as.get h


mutual
@[reducible] def AttrsetTy.denote : AttrsetTy → AttrsetT
  | .merged n t rest => List.cons (n, t) (rest.denote)
  | .empty => []

@[reducible] def Ty.denote : Ty → Type
  | .num => Number
  | .string => String
  | .bool => Bool
  | .lambda d r => d.denote → r.denote
  | .list a => List a.denote
  | .attrset (.merged n t rest) => HList.cons (n, t.denote) []
  | .attrset (.empty) => HList.nil

end

How do I properly denote a row type like attrset which is essentially a JSON-like structure?

[Eric Wieser]

Perhaps looking at the implementation of docs#Lean.Json can help?

[Eric Wieser]

I think AttrsetT is a typo there?

[Eric Wieser]

You might want to work with set_option autoImplicit false to catch this kind of error earlier

[Anders Christiansen Sørby]

It is not a typo. I only included parts of the source. AttrsetT should however be Type, but this code is not correct anyway, and I'm not sure if I'm way off.
Lean.Json is nice, but it is not a type checker or a term based language.

I'm trying to build a parser and type checker for a lambda calculus which includes

I'm trying to adapt this PHOAS article to row types
https://lean-lang.org/lean4/doc/examples/phoas.lean.html

My idea was to create a recursive type definition that can represent a JSON-like, nix expressions, structure including lambda expressions.
So for example

{a = true; "b" = "string"}

I can define a type L like this and map strings to types

def strToType : (s:String) → Type
  | "b" => String
  | "a" => Bool
  | _ => Unit

def L :Type := HList strToType ["b", "a"]

Or something like that. I was hoping someone with type theory experience can help me.

[Mario Carneiro]

the type of the lambda does not look like PHOAS

[Anders Christiansen Sørby]

{a = b: b}

would have a type

def strToType : (s:String) → Type
  | "a" => Any -> Any
  | _ => Unit

def L :Type := HList strToType ["a"]

[Anders Christiansen Sørby]

I almost got this working now :) I just need to prove termination. Any tips on how to do that?

@[reducible] def Ty.denote : (ty : Ty) → Type
  | .num => Number
  | .string => String
  | .bool => Bool
  | .lambda d r => d.denote → r.denote
  | .list a => List a.denote
  | .attrset maps names => HList (Ty.denote ∘ maps) names

[James Gallicchio]

with mutual and nested inductives, it can be pretty hard to prove termination

[James Gallicchio]

for the attrset case, you will essentially need to get a proof term passed to Ty.denote which says that the value being passed into it from maps is smaller than ty. and then you can use the termination_by syntax to prove termination

[James Gallicchio]

there is an autogenerated notion of size called sizeOf (from the typeclass SizeOf) which might work for you. otherwise you'll have to define your own measure of size on Tys

[Anders Christiansen Sørby]

I've gotten this far

@[reducible] def Ty.denote : (ty : Ty) → Type
  | .num => Number
  | .string => String
  | .bool => Bool
  | .lambda d r => d.denote → r.denote
  | .list a => List a.denote
  | .attrset maps names => HList (Ty.denote ∘ maps) names

termination_by denote ty =>
    by {
      cases ty with
      | attrset maps names =>
        apply sizeOf maps
      | lambda d r =>
        apply sizeOf d
      | _ => apply 0
    }

But it fails for the lambda case

Header

failed to prove termination, possible solutions:
- Use have-expressions to prove the remaining goals
- Use termination_by to specify a different well-founded relation
- Use decreasing_by to specify your own tactic for discharging this kind of goal

d r: Ty
⊢ rec PUnit.unit (fun name type rest type_ih rest_ih => PUnit.unit) (fun h => 0) (fun h => 0) (fun h => 0)
(fun a a_1 a_ih a_ih h => sizeOf a) (fun a a_ih h => 0) (fun maps names maps_ih h => 0) d (_ : d = d) <
sizeOf d

[James Gallicchio]

If you haven't yet, check out FPIL's section on proving termination

[James Gallicchio]

oh, it doesn't actually have examples of putting haves in the body. let me look around for examples...

[James Gallicchio]

basically you need a have : the termination goal := proof in scope at the recursive calls

[Anders Christiansen Sørby]

Thanks. I will try.

[Anders Christiansen Sørby]

I haven't been so successful proving termination. It seems like all the recursive terms are hard to show termination of. The proof needs to know that the recursion will never grow larger than Ty and shrink as the tree is traversed.

@[reducible] def Ty.denote : Ty → Type
  | .num => Number
  | .string => String
  | .bool => Bool
  | .attrset maps names =>
    HList (Ty.denote ∘ maps) names
  | .list a =>
    have : sizeOf a < sizeOf (list a) := by {
      simp [Nat.lt_succ_self, Nat.add_comm 1, Nat.lt_add_left]
    }
    List a.denote
  | .lambda d r =>
    have : sizeOf d < sizeOf (Ty.lambda d r) := by {
      simp [Nat.lt_succ_self,Nat.add_comm 1, Nat.lt_add_right]
    }
    d.denote → r.denote

termination_by denote ty =>
    by {
      cases ty with
      | attrset maps names =>
        apply sizeOf names
      | lambda d r =>
        apply sizeOf (lambda d r)
      | list a =>
        apply sizeOf a
      | _ => apply 0
    }

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal

maps: Name → Ty
names: List Name
a✝: Ty
⊢ rec PUnit.unit (fun name type rest type_ih rest_ih => PUnit.unit) (fun h => 0) (fun h => 0) (fun h => 0)
    (fun a a_1 a_ih a_ih h => 1 + sizeOf a + sizeOf a_1) (fun a a_ih h => sizeOf a)
    (fun maps names maps_ih h => sizeOf names) a✝ (_ : a✝ = a✝) <
  sizeOf names

Any suggestions?

[James Gallicchio]

have you tried defining it as two mutually recursive functions that match the mutually recursive structure of Ty and AttrsetTy?

mutual
def AttrsetTy.denote : AttrsetTy → Type
| ...

def Ty.denote : Ty → Type
| ...
end

[Anders Christiansen Sørby]

That was my initial attempt yes. But it didn't work out