Zulip Chat Archive

Stream: general

Topic: expose class func to top-level


view this post on Zulip Zesen Qian (Jun 06 2018 at 19:50):

Hi, how can I expose a function defined in type class to the top-level? i.e., the way to_string is exposed.

view this post on Zulip Simon Hudon (Jun 06 2018 at 19:52):

You can do export has_to_string (to_string)

view this post on Zulip Zesen Qian (Jun 06 2018 at 19:55):

the function it exposes doesn't seem to the one I want. I have to provide the type parameter.

view this post on Zulip Zesen Qian (Jun 06 2018 at 19:55):

I hope I can write to_string 5 instead of to_string nat 5

view this post on Zulip Zesen Qian (Jun 06 2018 at 19:56):

ahh sorry, seem in my case, the type inference doesn't work; in other case it works well.

view this post on Zulip Simon Hudon (Jun 06 2018 at 19:58):

I think there are two ways of doing that. Either you write a definition in the global namespace where you have fine control over implicit / explicit parameters or you use the following:

class my_algebra (a : Type) :=
  (zero {} : a)

I haven't used it myself but I think it should work.

view this post on Zulip Simon Hudon (Jun 06 2018 at 19:59):

(I just tried it. It works)

view this post on Zulip Zesen Qian (Jun 06 2018 at 19:59):

thanks! now it works.

view this post on Zulip Zesen Qian (Jun 06 2018 at 20:00):

question: how to give the checker a hint for synthesis?

view this post on Zulip Simon Hudon (Jun 06 2018 at 20:00):

Do you mean elaboration, i.e. inferring the type that are not explicitly required?

view this post on Zulip Zesen Qian (Jun 06 2018 at 20:01):

yes. But in my case it can't be inferred, so I want to give it a hint of the type.

view this post on Zulip Simon Hudon (Jun 06 2018 at 20:02):

If your function is foo, @foo makes every implicit parameters (types, type class instances and others) explicit. It's a bit of all or nothing but there are ways to simplify if that comes up too often.

view this post on Zulip Simon Hudon (Jun 06 2018 at 20:04):

Sorry, my brain is currently working in Haskell. In Lean, if that comes up too often, you may have to make the parameter explicit. Before you get there, can give some type annotations in the form of (expr : type)

view this post on Zulip Simon Hudon (Jun 06 2018 at 20:06):

For example if your function infers a type from its list argument but you provide an empty list, you can write foo ([] : list a) or foo (@nil a)

view this post on Zulip Zesen Qian (Jun 06 2018 at 20:08):

yep! I just used annotation and it works well.


Last updated: May 11 2021 at 22:14 UTC