Joshua Grosso (Jul 13 2021 at 18:52): Joshua Grosso (Jul 13 2021 at 18:52):What's the best way to encode a Haskell-like functional dependency in a typeclass? (Is it perhaps to add the associated type as a member of the class's record, or would that not work properly with unification?)
Joshua Grosso (Jul 13 2021 at 20:35):Update: the "member of the class" idea is not interacting nicely with Hint Modes + or ! (- does work, interestingly). I have to explicitly cast elements of the associated type into @<associated type field name> <instance>, which is proving super-cumbersome.
Example:
Class foo B := {A : Type; bar : A -> B}.
Hint Mode foo ! : typeclass_instances.
#[global] Instance nat_foo : foo nat := {A := nat; bar x := x}.
Fail Compute (bar 1). (* The term "1" has type "nat" while it is expected to have type "A". *)
I was wondering if maybe the fact the class can only be determined by the return type is an issue, so I tried specifying (bar 1 : nat), but that didn't work.
Just for fun, I added an extra parameter of type B to bar, in case maybe that would help resolution, but that didn't work either.
However, if that extra parameter is the first parameter, it works. I can work with this restriction if necessary (define Notations and whatnot to make life easier), but is it necessary?
Joshua Grosso (Jul 13 2021 at 21:01):I think I might've figured out a solution, when I was reading the docs for Hint Mode. If I set the associated type's hint mode to -, and the others to + or !, it works (which makes sense, since it really is the only "input" parameter).
Paolo Giarrusso (Jul 17 2021 at 18:50):Yes, that sounds like the usual solution, even if it doesn't exactly encode functional dependencies. To use members like that, and have type inference handle them, you should use canonical structures, but those have different kinds of complexity
Last updated: Oct 13 2024 at 01:02 UTC