Canonicity, implicits and soundness

[typesanitizer]

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 different Ord implicits, leaving the map in an inconsistent state.

Do you enforce canonicity? Or is this possibility ruled out using some other mechanism?

[brendanzab]

I'm pretty sure @Marwes was planning to add generative modules for this 🤔

[Marwes]

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".

[brendanzab]

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.

[Marwes]

Ah, that's true as well. Generative modules on steroids in a sense.

[typesanitizer]

Maybe I'm misunderstanding something here.

1. When you say "generative modules", you mean "generative functors", correct?

2. 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.

[Marwes]

Yes, we mean "generative functors" in this case (they "generate" modules I suppose 🙄 )

[typesanitizer]

Apologies for being pedantic, this is still new territory for me ... you can never be too careful about terminology 😅

[Etherian]

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.

[puffnfresh]

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.

[brendanzab]

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.

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.

[Marwes]

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

[brendanzab]

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.