Open typesanitizer opened 5 years ago
I'm pretty sure @Marwes was planning to add generative modules for this 🤔
Yeah, generative modules is the only way I know to resolve this. Not something I have really looked into yet though.
Currently canonicity is "enforced" by "don't do that".
You can also do this by tagging data structures with the instance that constructed them, but this would require being able to put values at the type level.
Ah, that's true as well. Generative modules on steroids in a sense.
Maybe I'm misunderstanding something here.
When you say "generative modules", you mean "generative functors", correct?
If you look at the paper, it uses the following example with Set
being an applicative functor -
module Set ( O : Ord ) : sig
type elt
type t
val empty : t
val add : elt -> t -> t
[...]
end
val add : { O : Ord } -> O.t -> Set(O).t -> Set(O).t
If Set
was a generative functor, then in the signature of the add
with the implicit O
, the two different Set(O).t
's would be different abstract types, and so you wouldn't be able to get its definition to type-check.
Yes, we mean "generative functors" in this case (they "generate" modules I suppose 🙄 )
Apologies for being pedantic, this is still new territory for me ... you can never be too careful about terminology 😅
You can also do this by tagging data structures with the instance that constructed them, but this would require being able to put values at the type level.
That seems to be the method used in this implementation of a Map in Idris.
I don't understand all that fancy "generative functor" stuff, but it looks like you could add a wrapper around the tree to hold its canonical Ord
instance then modify the functions to use that stored instance. That said, I haven't checked if that would break anything or make Map
awkward to work with.
I don't think empty :: forall a. Set a
should become empty :: forall a. Ord a => Set a
- it doesn't actually use the Ord. We've lost some parametricity.
I think we also focus on the Map, Set, etc. examples but these are just examples; more complicated cases of coherency appear.
I don't think
empty :: forall a. Set a
should becomeempty :: forall a. Ord a => Set a
- it doesn't actually use the Ord. We've lost some parametricity.
To clarify, we are more saying that empty :: forall a. Set a
should become something like empty :: forall a. (o :: Ord a) => Set a o
, because future operations on Set
require the same Ord
instance to used. Note the o
parameter on Set a o
. Perhaps you could come up some way of 'upgrading' empty sets to also take on a specific Ord
instance though - I dunno.
The empty set is the one set that actually is independent of the the ord instance though. Which is what @puffnfresh is saying. Regardless of how canonicity is solved that may be a good thing to preserve. I'd expect that to be solvable within generative functors as well, that is, just don't parameterise empty
With generative functors, you get a new type and the associated functions (like empty
, merge
, etc.) for each application of the Set
functor to an Ord
instance. This is kind of like each function in that module has the Ord
instance on it, without having to tediously thread the o
parameter around.
Unlike in the modular implicits paper (which has an example with sets), the map type in Gluon's stdlib isn't generated by functor application, and doesn't "carry an Ord implementation". Consequently, if you don't enforce canonicity somehow, then two different calls to
insert
could end up using differentOrd
implicits, leaving the map in an inconsistent state.Do you enforce canonicity? Or is this possibility ruled out using some other mechanism?