Help compiling simple finally tagless DSL

Stream: general

[Yuri de Wit]

As a learning experiment, I am trying to define a finally tagless DSL for XML and custom notations to clean up the authoring of XML docs within Lean.

However, I am getting an error I may need help digesting it:

failed to synthesize instance
  Xml ?m.631

Shouldnt I be able to start creating Xml "sentences" (see sampleXml below) in this DSL even before providing a concrete implementation?

inductive XmlCat where
  | ROOT
  | CHILD
  | ATTR

open XmlCat

class Xml (repr: XmlCat -> Type) where
  text : (t : String) -> repr CHILD
  attr : (n : String) -> (v : String) -> repr ATTR
  element : (n : String) -> (attrs : Array (repr ATTR) := #[]) -> (children : Array (repr CHILD) := #[]) -> repr CHILD

def sampleXml := Xml.text "aaa"

[Arthur Paulino]

This is Lean 4, right?

[Henrik Böving]

Certainly looks like it based on the naming scheme and Array

[Henrik Böving]

the issue this doesnt work is that the text constructor expects the elaborator to be capable of inferring what CHILD should be, but it is not in this case since it does not have enough information, if you made this possible for it it would be perfectly capable of constructing this value.

[Yuri de Wit]

Yes, Lean4.

[Yuri de Wit]

Henrik Böving said:

the text constructor expects the elaborator to be capable of inferring what CHILD should be

But isnt CHILD a concrete XmlCat constructor?

[Yuri de Wit]

The other part to this would be to provide a concrete implementation:

structure R (c : XmlCat) where
  unR : String

instance : ToString (R a) where
  toString r := r.unR

instance : Xml R where
  text t := { unR := t}
  attr n v := { unR := s!"{n}={v}" }
  element n attrs children := { unR := s!"<{n}" }

def t : R CHILD := text "aaa"

And this works.

Is this mainly a matter or not having type inference like Haskell does?

[Reid Barton]

Yes, looks like it

[Reid Barton]

In particular, Lean can't infer class constraints (afaik still true in Lean 4)

[Yuri de Wit]

Ok, that makes sense. And that also means I am able to define a function that is polymorphic on repr, explicitly:

def t [Xml r] : (r CHILD) := text "aaa"

And this also works!

The puzzling thing at first was getting an error when trying repr instead of r (in fact any any identifier greater than one char seems to cause problems):

def t [Xml repr] : (repr CHILD) := text "aaa" -- error: "application type mismatch  Xml repr argument  repr has type  m.628 → Format : Type ?u.627 but is expected to have type  XmlCat → Type : Type 1Lean 4"

def t [Xml aa] : (aa CHILD) := text "aaa" -- error: "unknown identifier"

What else is happening here?

[Reid Barton]

I think single letter identifiers implicitly get turned into (implicit) arguments but longer identifiers don't--may have the details wrong about this.

[Yuri de Wit]

(btw, maybe I should be posting in lean4?)