Stream: General

Topic: Construct term while instantiating schematic type variables


view this post on Zulip Lukas Stevens (Aug 04 2020 at 14:46):

I have this situation:

val term = ...
val app_term = term $ t1 $ t2

term contains schematic type variables. Is there a function that constructs app_term with instantiated schematic type variables?

view this post on Zulip Lukas Stevens (Aug 04 2020 at 14:50):

The instantiation should use the types of t1 and t2 accordingly.

view this post on Zulip Manuel Eberl (Aug 04 2020 at 14:58):

Hmm, I think maybe you want type inference. Don't know all that much about it though to be honest. Maybe search for "schematic" in the Isabelle cookbook.

view this post on Zulip Manuel Eberl (Aug 04 2020 at 14:58):

(inb4 have fun with flex-flex pairs :D)

view this post on Zulip Lukas Stevens (Aug 04 2020 at 15:04):

there should'nt be any flex-flex pairs since there is only one schematic type variable that only occurs in term :fingers_crossed:

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:07):

if "term" is something whose type you know, I would just compute the type

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:08):

e.g. if "term" where addition, you should write an ML function mk_add : typ -> term that does something like mk_add T = Const (@{const_name "Groups.add"}, T --> T --> T).

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:08):

That's the way it's done in the library.

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:08):

I'd only use actual type inference with schematic variables and whatever if you absolutely have to

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:09):

Depends a bit where this "term" thing comes from, I guess.

view this post on Zulip Lukas Stevens (Aug 04 2020 at 15:09):

Ok, I'll try to do it without type inference, thanks for the hint.

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:11):

one common pattern is also to specify the type of the function as dummyT and then do a Syntax.check_term to let type inference fill in the type

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:12):

that doesn't seem to work in the presence of schematic variables though and I never really understood why

view this post on Zulip Manuel Eberl (Aug 04 2020 at 15:12):

I think you have to tag them somehow to tell type inference that it is allowed to fill them in

view this post on Zulip Lukas Stevens (Aug 04 2020 at 15:50):

Manuel Eberl said:

one common pattern is also to specify the type of the function as dummyT and then do a Syntax.check_term to let type inference fill in the type

Cool, I am using that now.


Last updated: Aug 15 2022 at 02:13 UTC