Interaction between Dependent Haskell quantifiers and instance contexts

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Interaction between Dependent Haskell quantifiers and instance contexts

Richard Eisenberg-4
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

> On Jun 28, 2018, at 7:30 PM, Andrew Martin <[hidden email]> wrote:
>
> 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
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Interaction between Dependent Haskell quantifiers and instance contexts

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

On Thu, Jun 28, 2018 at 11:49 PM, Richard Eisenberg <[hidden email]> wrote:
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

> On Jun 28, 2018, at 7:30 PM, Andrew Martin <[hidden email]> wrote:
>
> 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
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries




--
-Andrew Thaddeus Martin

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries