forall in constraint

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

forall in constraint

Alan & Kim Zimmerman
I am working on the Trees that Grow stuff, and hit a small problem

I have

type family XIB               x thing
type family XNewImplicitBndrs x thing

type ForallXImplicitBndrs (c :: * -> Constraint) (x :: *) (thing :: *) =
       ( c (XIB               x thing)
       , c (XNewImplicitBndrs x thing)
       )

and I want to extend the DataId constraint

type DataId p =
  ( Data p

  , ForallXImplicitBndrs Data p thing
  )

But the problem is I do not have `thing` at this point, and to get it in the code will involve some hs-boot nastiness.

Is there any way to require "forall thing. Data thing" inside the DataId constraint?

Alan

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

Re: forall in constraint

Li-yao Xia-2
Hi Alan,

One way is to define a new typeclass.


type ImplicitBndrs c x thing
   = (c (XIB x thing), c (XNewImplicitBndrs x thing))

class ForallImplicitBndrs c x where
   withImplicitBndrs
     :: forall thing. (ImplicitBndrs c x thing => t) -> t


Although that requires you to write one instance for every combination
of (c, x).
The "universal instance" of ImplicitBndrs can also be wrapped in the
Dict type in the constraints library. In fact, constraints has an even
more general mechanism for all of this in Data.Constraint.Forall. Pro:
no extra instances are necessary, so it is more easily extensible. Con:
internally relies heavily on unsafeCoerce, although the above is already
stretching the language a lot.

We start by defining a "class synonym" instead of a type synonym, to
enable partial application.


class (c (XIB x thing), c (XNewImplicitBndrs x thing))
   => ImplicitBndrs c x thing
instance (c (XIB x thing), c (XNewImplicitBndrs x thing))
   => ImplicitBndrs c x thing


-- "forall thing. ImplicitBndrs c x thing"
type ForallImplicitBndrs c x = Forall (ImplicitBndrs c x)

withImplicitBndrs
   :: forall c x thing
   .  ForallImplicitBndrs c x
   => (ImplicitBndrs c x thing => t) -> t
withImplicitBndrs t = case inst @(ImplicitBndrs c x) @thing of
   Sub Dict -> t


I think the ICFP paper "Quantified class constraints" talks about a more
principled future solution, and there is an old GHC ticket or two about it.

Cheers,
Li-yao


On 10/23/2017 11:06 AM, Alan & Kim Zimmerman wrote:

> I am working on the Trees that Grow stuff, and hit a small problem
>
> I have
>
> type family XIB               x thing
> type family XNewImplicitBndrs x thing
>
> type ForallXImplicitBndrs (c :: * -> Constraint) (x :: *) (thing :: *) =
>         ( c (XIB               x thing)
>         , c (XNewImplicitBndrs x thing)
>         )
>
> and I want to extend the DataId constraint
>
> type DataId p =
>    ( Data p
>
>    , ForallXImplicitBndrs Data p thing
>    )
>
> But the problem is I do not have `thing` at this point, and to get it in
> the code will involve some hs-boot nastiness.
>
> Is there any way to require "forall thing. Data thing" inside the DataId
> constraint?
>
> Alan
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171023/77c963b5/attachment.html>
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: forall in constraint

GHC - devs mailing list
In reply to this post by Alan & Kim Zimmerman

I’m lost. Could you give me a bit more context?

 

I’m deeply suspicious about that ForallXImplicitBndrs thing with strange higher kinded parameters.   Smells all wrong to me.

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Alan & Kim Zimmerman
Sent: 23 October 2017 16:07
To: [hidden email]
Subject: forall in constraint

 

I am working on the Trees that Grow stuff, and hit a small problem

I have

type family XIB               x thing
type family XNewImplicitBndrs x thing

type ForallXImplicitBndrs (c :: * -> Constraint) (x :: *) (thing :: *) =
       ( c (XIB               x thing)
       , c (XNewImplicitBndrs x thing)
       )

and I want to extend the DataId constraint

type DataId p =
  ( Data p

  , ForallXImplicitBndrs Data p thing
  )

But the problem is I do not have `thing` at this point, and to get it in the code will involve some hs-boot nastiness.

Is there any way to require "forall thing. Data thing" inside the DataId constraint?

Alan


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

Re: forall in constraint

Alan & Kim Zimmerman
In Shayan's implementation he has [1]

data ImplicitBndrs x thing
  = IB
      (XIB x thing)
      thing

  | NewImplicitBndrs
      (XNewImplicitBndrs x thing)

type family XIB               x thing
type family XNewImplicitBndrs x thing

type ForallXImplicitBndrs c x thing =
       ( c (XIB               x thing)
       , c (XNewImplicitBndrs x thing)
       )

This gets used, in the same file as

type LSigType   x = ImplicitBndrs x (LType x)

where `thing` is resolved to a specific type.

Because it is all in the same file, there is no problem making a
constraint on anything using LSigType, that mentions LHsType.



But in the approach I am taking[2], the type families are defined in
HsExtension, which is compiled early in the cycle, and imported by
HsTypes, HsBinds, HsDecl etc.

In order to derive a Data instance for anything using `LSigType x`, we
need to be able to specify that a Data instance exists for `LHsType x`.

So we can either do that directly in HsBinds, or try to add it to the existing
DataId constraint in HsExtension.

The first approach leads to a spread of the constraint throughout the AST,
which gets very messy.

The second approach requires being able to specify a
`forall thing. Data thing` constraint in HsExtension.


I tried an intermediate approach, introducing a constraint in HsDecls[3] to capture this,
but it eventually runs into needing it in the HsExpr.hs-boot file, which means I need
LHsType in that file.

Perhaps the simplest way forward is to get rid of the `thing` parameter completely,
and introduce the three or so ImplicitBinders variants that are used.

I hope this does not just confuse things even more.

Alan
[3] https://github.com/ghc/ghc/commit/22812296818fe955752fa4762cf72250abd09bf9#diff-7cfa6eef12e44d312aca9ef4af0081b3R1439



On 23 October 2017 at 23:04, Simon Peyton Jones <[hidden email]> wrote:

I’m lost. Could you give me a bit more context?

 

I’m deeply suspicious about that ForallXImplicitBndrs thing with strange higher kinded parameters.   Smells all wrong to me.

 

Simon



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

RE: forall in constraint

GHC - devs mailing list
  • Like I say I am DEEPLY suspicious of ForallXImplicitBndrs.  I can’t make head or tail of it.  Is see in you patch you define

type ForallXPat (c :: * -> Constraint) (x :: *) =…

 

               What is this?  Why do we need it? What goes wrong if we remove it altogether?

 

  • Likewise `forall thing. Data thing` makes no sense to me as a constraint,  even with quantified context. Shayan and I discussed this at ICFP and agreed it made no sense.  The hoped-for quantified-context extension is NOT a solution.

 

Overall I’ve lost track of these enormous constraint tuples that seem to be associated with Data instances. Can you give a small artificial (ie not full GHC) example of why they are necessary?   Perhaps it’s this

 

data T p = T1 (XT1 p) Int
                | T1 (XT2 p) (IdP p)

 

I suppose that a Data instance would need to have

               instance (Data (XT1 p), Data (XT2p), Data (IdP p)) => Data IT p) where…

Is that right?  In which case why do you have all this PostRn stuff in the DataId type?  (And why is it called DataId?)

 

  • “The first approach leads to a spread of the constraint throughout the AST, which gets very messy.”  I don’t understand what the first approach is, or why it gets messy.  Could you be more concrete?
  • “Perhaps the simplest way forward is to get rid of the `thing` parameter completely, and introduce the three or so ImplicitBinders variants that are used.”   I don’t’ think it could possibly make anything simpler to have three separate data types.   Can you illustrate concretely?  

It’d be great to explore these issues with small, concrete examples, rather than the full glory of GHC, both for our own benefit and the benefit of those who will review the patch and (in future) understand the code.

 

Sorry to be slow

 

Simon

 

 

From: Alan & Kim Zimmerman [mailto:[hidden email]]
Sent: 23 October 2017 22:36
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]
Subject: Re: forall in constraint

 

In Shayan's implementation he has [1]

data ImplicitBndrs x thing
  = IB
      (XIB x thing)
      thing

  | NewImplicitBndrs
      (XNewImplicitBndrs x thing)

type family XIB               x thing
type family XNewImplicitBndrs x thing

type ForallXImplicitBndrs c x thing =
       ( c (XIB               x thing)
       , c (XNewImplicitBndrs x thing)
       )

This gets used, in the same file as

type LSigType   x = ImplicitBndrs x (LType x)

where `thing` is resolved to a specific type.

 

Because it is all in the same file, there is no problem making a

constraint on anything using LSigType, that mentions LHsType.

 

 

 

But in the approach I am taking[2], the type families are defined in
HsExtension, which is compiled early in the cycle, and imported by
HsTypes, HsBinds, HsDecl etc.

 

In order to derive a Data instance for anything using `LSigType x`, we

need to be able to specify that a Data instance exists for `LHsType x`.

 

So we can either do that directly in HsBinds, or try to add it to the existing

DataId constraint in HsExtension.

 

The first approach leads to a spread of the constraint throughout the AST,

which gets very messy.

 

The second approach requires being able to specify a

`forall thing. Data thing` constraint in HsExtension.

 

 

I tried an intermediate approach, introducing a constraint in HsDecls[3] to capture this,

but it eventually runs into needing it in the HsExpr.hs-boot file, which means I need

LHsType in that file.

 

Perhaps the simplest way forward is to get rid of the `thing` parameter completely,
and introduce the three or so ImplicitBinders variants that are used.

 

I hope this does not just confuse things even more.

 

Alan

[3] https://github.com/ghc/ghc/commit/22812296818fe955752fa4762cf72250abd09bf9#diff-7cfa6eef12e44d312aca9ef4af0081b3R1439

 

 

 

On 23 October 2017 at 23:04, Simon Peyton Jones <[hidden email]> wrote:

I’m lost. Could you give me a bit more context?

 

I’m deeply suspicious about that ForallXImplicitBndrs thing with strange higher kinded parameters.   Smells all wrong to me.

 

Simon

 


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