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 <rae at cs.brynmawr.edu>
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 <andrew.thaddeus at gmail.com>
> 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
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>


-- 
-Andrew Thaddeus Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180629/1761b9b8/attachment.html>