Zulip Chat Archive

Stream: general

Topic: Default arguments with type parameter


view this post on Zulip Keeley Hoek (Aug 18 2018 at 10:42):

I've got a (honest, in-a-program) function

def do_some_stuff {α : Type} (cfg : config α) := xxx

In an ideal world, I'd like to be able to have a default config, with a fixed parameter α (obviously), so I could write do_some_stuff and everything would work great. I guess I want to be able to write (and compile)

def default_config : config string := xxx
def do_some_stuff {α : Type} (cfg : config α := default_config) := xxx

with that having the meaning that if cfg is omitted, the type α is forced to be string.

I see that I might be "fighting the system". What do you think is the best way to emulate this kind of option-passing interface?

view this post on Zulip Mario Carneiro (Aug 18 2018 at 11:50):

This comes up in core lean in some of the structures, where you have to give A such that A = B, and the proof of A = B is rfl but this only works if A is B. You can set this up using auto params instead of opt params:

def config : Type → Type := sorry
def default_config : config string := sorry
meta def default_config_tac : tactic unit := `[exact default_config]
def do_some_stuff {α : Type} (cfg : config α . default_config_tac) : α := sorry

example : string := do_some_stuff -- ok
example : nat := do_some_stuff (sorry : config ℕ) -- ok
example : nat := do_some_stuff -- error

view this post on Zulip Keeley Hoek (Aug 18 2018 at 11:56):

Thanks so much Mario. Do you know where I could read about the auto params "." period syntax?

view this post on Zulip Mario Carneiro (Aug 18 2018 at 11:57):

It might be in the reference manual? It's very simple. You can only put a name of a def of a tactic unit there, and it gets called when the argument is not supplied

view this post on Zulip Mario Carneiro (Aug 18 2018 at 11:57):

I wish it would accept an expression so you could write a tactic inline there, but alas

view this post on Zulip Keeley Hoek (Aug 18 2018 at 11:58):

ok sweet! cheers!

view this post on Zulip Mario Carneiro (Aug 18 2018 at 11:58):

(actually there is a good reason you can't write a tactic inline, since that would be meta)


Last updated: May 11 2021 at 22:14 UTC