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

[Richard Eisenberg]

I think that will be fine. It will mean that the instance can be used only where n is bound relevantly, but you probably knew that. I simply don't see any problems here.

Richard

Post by 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.
data Nat
data Natty :: Nat -> Type
class NATTY (n :: Nat)
data Vec :: Nat -> Type -> Type
instance NATTY n => Applicative (Vec n)
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
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

[Andrew Martin]

Thanks, that alleviates my concern. I'm glad to hear this should be
possible.

Post by Richard Eisenberg
I think that will be fine. It will mean that the instance can be used only
where n is bound relevantly, but you probably knew that. I simply don't see
any problems here.
Richard

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.

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

data Vec :: Nat -> Type -> Type
instance NATTY n => Applicative (Vec n)
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
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries