Zulip Chat Archive

Stream: lean4

Topic: tagless final (simple) type inference


Yuri de Wit (Jun 08 2022 at 12:29):

We discussed this a few months back, but I am only now circling back.

I am experimenting with Oleg Kiselyov's paper Typed Tagless Final Interpreters and have a simple question.

Consider the following #mwe:

inductive NodeTree where
  | Attr
  | Node

class Markup (repr : NodeTree -> Type) where
  elem : String  (attrs : Array (repr .Attr) := #[])  (children : Array (repr .Node) := #[])  repr .Node
  attr : (name : String) -> (value : String := "") -> repr .Attr
  text : String  repr .Node

open Markup

def anHtmlDoc [Markup m] : m .Node := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]

This works and I am able to create multiple representations for the same anHtmlDoc.

My question is whether Lean is/should be supposed to infer that anHtmlDoc is a Markup of kind .Node, since it seems a bit redundant and effectively unused here. It would be great if this could work:

def anHtmlDoc [Markup m] : m _ := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]

But the above gives me the following error:

don't know how to synthesize placeholder
context:
m : NodeTree  Type
inst : Markup m
 NodeTree
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

If I a follow what the error suggests and remove the resulting type (I guess this would be an even better, simpler solution):

def anHtmlDoc := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]

But, unfortunately, I get:

failed to synthesize instance
  Markup ?m.195

Sebastian Ullrich (Jun 08 2022 at 12:41):

You can move the type annotation into the body

def anHtmlDoc [Markup m] := show m _ from elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]

Yuri de Wit (Jun 08 2022 at 13:27):

Thanks, I did no know about show _ from!

So, in theory, there could be various ways of achieving this, but only the last two actually work today.

def anHtmlDoc := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]
def anHtmlDoc [Markup m] : m _ := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]
def anHtmlDoc [Markup m] : m .Node := elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]
def anHtmlDoc [Markup m] := show m _ from elem "tag" #[(attr "name1" "vv")] #[elem "c1", text "some content"]

Are the plans to make the first two also typecheck in the future?


Last updated: Dec 20 2023 at 11:08 UTC