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