<div dir="ltr">Thanks, that alleviates my concern. I'm glad to hear this should be possible.</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jun 28, 2018 at 11:49 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
Richard<br>
<div><div class="h5"><br>
> On Jun 28, 2018, at 7:30 PM, Andrew Martin <<a href="mailto:andrew.thaddeus@gmail.com">andrew.thaddeus@gmail.com</a>> wrote:<br>
> <br>
> 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.<br>
> <br>
> Consider the following types from Hasochism:<br>
> <br>
> data Nat<br>
> data Natty :: Nat -> Type<br>
> class NATTY (n :: Nat)<br>
> <br>
> 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:<br>
> <br>
> data Vec :: Nat -> Type -> Type<br>
> instance NATTY n => Applicative (Vec n)<br>
> <br>
> To handle this with dependent types, we would need to instead write:<br>
> <br>
> instance pi n. Applicative (Vec n)<br>
> <br>
> 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.<br>
> <br>
> Sent from my iPhone<br>
</div></div>> ______________________________<wbr>_________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
<br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">-Andrew Thaddeus Martin</div>
</div>