Interaction between Dependent Haskell quantifiers and instance contexts

[Andrew Martin]

In Richard Eisenberg’s PhD thesis Dependent Types in Haskell: Theory and Practice, he presents outline of what dependent types in Haskell would look like. Such an extension to GHC Haskell would replace most uses of the singleton design pattern described by the Hasochism paper (McBride). But, there is one use of singletons (the design pattern, not the library) that Eisenberg’s thesis doesn’t touch on: using pi types in typeclass instances contexts.

Consider the following types from Hasochism:

data Nat
data Natty :: Nat -> Type
class NATTY (n :: Nat)

The first type is peano numbers. The second type is a singleton type. The third is a class used to implicitly provide values of type Natty in instance contexts. The same paper puts this class to good use when defining an Applicative instance for length indexed vectors:

data Vec :: Nat -> Type -> Type
instance NATTY n => Applicative (Vec n)

To handle this with dependent types, we would need to instead write:

instance pi n. Applicative (Vec n)

I haven’t seen or heard any talk about whether this will be admissible. I’d be interested in hearing thoughts from the cognoscenti about any fundamental barriers (either theoretical or GHC-specific) that would prevent something like this from being admitted. I have typeclass instances like this come up fairly often in code I work on, so it’s not just a theoretical question to me. Being able to do this really would help me cut down on boilerplate.

Sent from my iPhone