5 ms·

Having canonical implementations is a feature, not a bug, of type-classes. For example, consider the type `Data.MaxHeap a`, which is a persistent max-priority

Having canonical implementations is a feature, not a bug, of type-classes. For example, consider the type `Data.MaxHeap a`, which is a persistent max-priority heap. Max-heaps can be combined in logarithmic time, as long as they are ordered internally by the same ordering. Haskell provides `Data.Heap.union :: Ord a => MaxHeap a -> MaxHeap a -> MaxHeap a`. This is only possible because the type guarantees that the ordering of the two MaxHeaps is the same (the one single implementation of `Ord a`). It also means that you don't have to store any v-table within the `MaxHeap` value, making lookup just a bit faster and making optimizations like monomorphization easier. If you didn't have canonical implementations, you would have to give up being able to write safe & efficient data-structures like this. You would need to be able to dynamically store orderings (wasting space), dynamically compare orderings (wasting time), and have redundant failure paths only for the extremely uncommon and undesirable case where you try to `union` two MaxHeaps with different internal orderings (MaxHeap a -> MaxHeap a -> Maybe (MaxHeap a)). ----- An alternative might be dependent types, where you can instead insist that the ordering _values_ within the two heaps are compatible, gaining the efficiency (by using "ghost" variables) and safety of canonical implementations while avoiding the , but this is more complicated to use, and Haskell doesn't have proper dependent types (yet?). ---- However, in most situations where you might want to try violating canonical instances, defining a newtype is a perfectly satisfactory way to do it.

jules 5y ago
If you compare it with how you'd implement such a data structure using ML modules, it becomes very clear that the bug here is the definition of Data.Heap.Union, not the non-canonicity of type classes. With ML modules you'd define a Heap module that is parameterised by an Ord module. Different instantiations of the Heap module for the same type `a` but different instances of `Ord a` are different: heaps with Ord1 are of a different type than heaps of Ord2. From this point of view, passing the Ord instance into each individual heap function call (such as union) is clearly not the right setup. The canonicity of type classes is merely a bandaid for that problem.
- tel 5y ago
  Generative functors indeed fixes the issue, but it’s kind of interesting because they’re similar in a way to newtypes. In each case, you generate a new type, distinct from the others, which holds a new implementation of the same interfaces. It comes down to ergonomics where OCaml’s approach tends to make local reasoning easier and Haskell’s approach makes it a little easier to transform structurally isomorphic types into one another by wrapping/unwrapping.
  - jules 5y ago
    Probably the last word on this problem hasn't been said, because all approaches seem to have some downsides. Could you give an example where Haskell's approach makes it easier?
- curtisf 5y ago
  Is this not just moving the problem to a different place? (Maybe it's more ergonomic for some uses) In Haskell the solution is to use different type parameters via newtypes. In ML, you define a distinct instantiation of the MaxHeap. So the difference (in Haskell terms) is something like `HeapInstantiation1` vs `Heap Wrapped1` Is this practically a big enough difference to call the Haskell approach wrong? Is it not useful to have a single instantiation able to handle all parameters?
  - jules 5y ago
    I think one practical disadvantage of the Haskell approach is that you need to wrap and unwrap your types if you want a different ordering on an existing type. But the main reason why I didn't like the Haskell approach isn't ergonomic but conceptual. To me, the type of the heap should depend on the Ord instance, because the invariant satisfied by the values of type `Heap a` depends on the Ord instance of `a`, not just on the type `a` itself. This invariant is not encoded in the type system in Haskell, but in a dependently typed language you could do that. But in order to even write down the invariant, you need access to the Ord instance. So the type signature of union could be: union : {a:Type} → {o:Ord a} → Heap o → Heap o → Heap o In this case the problem of mixing up heaps with different orderings is ruled out by ordinary type checking, rather than via an extra meta-theoretical invariant satisfied by the language. Although ML modules don't let you encode the invariant either, they at least set it up in the same way, because the type Heap(o).t depends on the o and not just on o.t, and the type checker also views it that way and will say Heap(o).t ≠ Heap(o').t even when o.t = o'.t. In Haskell on the other hand, if we desugar type classes to passing around records, then we can suddenly break the invariant in type safe code. Maybe I'm imposing values on Haskell that have no practical significance in that context, but to me the way Haskell does it feels like a hack.
volta83 5y ago
> If you didn't have canonical implementations, you would have to give up being able to write safe & efficient data-structures like this. No? Just make the type generic on the ordering. Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) or something like that.
- curtisf 5y ago
  I explained why this doesn't work -- what do you do when you combine two heaps with different internal orderings? You need some way to enforce that the orderings are the _same_. A canonical ordering per type is how Haskell does it; dependent types are a more complicated alternative method.
  - remexre 5y ago
    I think GP is suggesting... well, dependent types, but in a restricted enough way that I don't believe it adds additional complexity over DataKinds. At least, I read > Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) as saying the kind of MaxHeap should be, in Coq syntax, (forall (T : Set), (T -> T -> Bool)). I think this doesn't add any additional complexity vs DataKinds since the function doesn't need to be evaluable at typechecking time, just unified against at construction-time.
  - volta83 5y ago
    > You need some way to enforce that the orderings are the _same_ Just require that the Ord type is the same for all heaps ? MaxHeap(MaxHeap(T, MyOrd), MyOrd) uses the same ordering, but MaxHeap(MaxHeap(T, Ord0), Ord1) does not.
    - volta83 5y ago
      A simple way to do this is to: MyNestedMaxHeap(T, Ord) = MaxHeap(MaxHeap(T, Ord), Ord) such that when using MyNestedMaxHeap only one Ord type can be passed.
remexre 5y ago
Does it break anything to allow datatypes to be parametric over instances? eg instance absOrd : Ord Int where -- ... union :: (ord : Ord a) => MaxHeap a ord -> MaxHeap a ord -> MaxHeap a ord If it's still impossible to create instances at runtime, I don't think this is equivalent to proper dependent types, only DataKinds.

jules 5y ago

If you compare it with how you'd implement such a data structure using ML modules, it becomes very clear that the bug here is the definition of Data.Heap.Union, not the non-canonicity of type classes. With ML modules you'd define a Heap module that is parameterised by an Ord module. Different instantiations of the Heap module for the same type `a` but different instances of `Ord a` are different: heaps with Ord1 are of a different type than heaps of Ord2. From this point of view, passing the Ord instance into each individual heap function call (such as union) is clearly not the right setup. The canonicity of type classes is merely a bandaid for that problem.

tel 5y ago
Generative functors indeed fixes the issue, but it’s kind of interesting because they’re similar in a way to newtypes. In each case, you generate a new type, distinct from the others, which holds a new implementation of the same interfaces. It comes down to ergonomics where OCaml’s approach tends to make local reasoning easier and Haskell’s approach makes it a little easier to transform structurally isomorphic types into one another by wrapping/unwrapping.
- jules 5y ago
  Probably the last word on this problem hasn't been said, because all approaches seem to have some downsides. Could you give an example where Haskell's approach makes it easier?
curtisf 5y ago
Is this not just moving the problem to a different place? (Maybe it's more ergonomic for some uses) In Haskell the solution is to use different type parameters via newtypes. In ML, you define a distinct instantiation of the MaxHeap. So the difference (in Haskell terms) is something like `HeapInstantiation1` vs `Heap Wrapped1` Is this practically a big enough difference to call the Haskell approach wrong? Is it not useful to have a single instantiation able to handle all parameters?
- jules 5y ago
  I think one practical disadvantage of the Haskell approach is that you need to wrap and unwrap your types if you want a different ordering on an existing type. But the main reason why I didn't like the Haskell approach isn't ergonomic but conceptual. To me, the type of the heap should depend on the Ord instance, because the invariant satisfied by the values of type `Heap a` depends on the Ord instance of `a`, not just on the type `a` itself. This invariant is not encoded in the type system in Haskell, but in a dependently typed language you could do that. But in order to even write down the invariant, you need access to the Ord instance. So the type signature of union could be: union : {a:Type} → {o:Ord a} → Heap o → Heap o → Heap o In this case the problem of mixing up heaps with different orderings is ruled out by ordinary type checking, rather than via an extra meta-theoretical invariant satisfied by the language. Although ML modules don't let you encode the invariant either, they at least set it up in the same way, because the type Heap(o).t depends on the o and not just on o.t, and the type checker also views it that way and will say Heap(o).t ≠ Heap(o').t even when o.t = o'.t. In Haskell on the other hand, if we desugar type classes to passing around records, then we can suddenly break the invariant in type safe code. Maybe I'm imposing values on Haskell that have no practical significance in that context, but to me the way Haskell does it feels like a hack.

volta83 5y ago

> If you didn't have canonical implementations, you would have to give up being able to write safe & efficient data-structures like this. No? Just make the type generic on the ordering. Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) or something like that.

curtisf 5y ago
I explained why this doesn't work -- what do you do when you combine two heaps with different internal orderings? You need some way to enforce that the orderings are the _same_. A canonical ordering per type is how Haskell does it; dependent types are a more complicated alternative method.
- remexre 5y ago
  I think GP is suggesting... well, dependent types, but in a restricted enough way that I don't believe it adds additional complexity over DataKinds. At least, I read > Instead of MaxHeap(T), make it MaxHeap(T, Ord:(T,T)->bool) as saying the kind of MaxHeap should be, in Coq syntax, (forall (T : Set), (T -> T -> Bool)). I think this doesn't add any additional complexity vs DataKinds since the function doesn't need to be evaluable at typechecking time, just unified against at construction-time.
- volta83 5y ago
  > You need some way to enforce that the orderings are the _same_ Just require that the Ord type is the same for all heaps ? MaxHeap(MaxHeap(T, MyOrd), MyOrd) uses the same ordering, but MaxHeap(MaxHeap(T, Ord0), Ord1) does not.
  - volta83 5y ago
    A simple way to do this is to: MyNestedMaxHeap(T, Ord) = MaxHeap(MaxHeap(T, Ord), Ord) such that when using MyNestedMaxHeap only one Ord type can be passed.

remexre 5y ago

Does it break anything to allow datatypes to be parametric over instances? eg instance absOrd : Ord Int where -- ... union :: (ord : Ord a) => MaxHeap a ord -> MaxHeap a ord -> MaxHeap a ord If it's still impossible to create instances at runtime, I don't think this is equivalent to proper dependent types, only DataKinds.