Can we offer ~ without GADTs or type families?

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

Can we offer ~ without GADTs or type families?

David Feuer

It seems to me that equality constraints could potentially be supported by an implementation with neither GADTs nor type families. Type families don't really seem to have much to do with it, and GADTs are strictly heavier (GADTs ~= ExistentialQuantification + TypeEquality).

Could we get a separate LANGUAGE pragma just for equality constraints?


_______________________________________________
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: Can we offer ~ without GADTs or type families?

Ryan Scott
Hi David,

> Could we get a separate LANGUAGE pragma just for equality constraints?

I think we should, and I don't think we'd even need to introduce a new
pragma, since there's already a perfectly good one: -XTypeOperators!
After all, there's nothing really that special about (~) other than
some typechecking details. A fix to Trac #9194 [1] would give us this.

Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/ticket/9194
_______________________________________________
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: Can we offer ~ without GADTs or type families?

Edward Kmett-2
TypeOperators as a language extension doesn't require a whole lot on the behalf of implementors today. They basically just have to add fixity handling to types. This is a no-brainer for a compiler implementor. It is a simple elaboration and some extra cases to deal with in their parser. The typechecker changes are obvious.

Asking them to do all the things to support 'some typechecking details' that aren't entirely trivial to support that same extension is an awful big ask! OutsideIn(X) is a big paper to read, let alone implement, and the only compiler to even try handling (~) today is GHC.

-Edward

On Fri, Aug 5, 2016 at 2:15 PM, Ryan Scott <[hidden email]> wrote:
Hi David,

> Could we get a separate LANGUAGE pragma just for equality constraints?

I think we should, and I don't think we'd even need to introduce a new
pragma, since there's already a perfectly good one: -XTypeOperators!
After all, there's nothing really that special about (~) other than
some typechecking details. A fix to Trac #9194 [1] would give us this.

Ryan S.
-----
[1] https://ghc.haskell.org/trac/ghc/ticket/9194
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
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: Can we offer ~ without GADTs or type families?

Ryan Scott
Good point, I hadn't considered the perspective of other compilers. In
that case, I could be persuaded to introduce a separate pragma like
-XTypeEqualities, and have -XGADTs and -XTypeFamilies imply
-XTypeEqualities for backwards compatibility.

Ryan S.

On Fri, Aug 5, 2016 at 2:27 PM, Edward Kmett <[hidden email]> wrote:

> TypeOperators as a language extension doesn't require a whole lot on the
> behalf of implementors today. They basically just have to add fixity
> handling to types. This is a no-brainer for a compiler implementor. It is a
> simple elaboration and some extra cases to deal with in their parser. The
> typechecker changes are obvious.
>
> Asking them to do all the things to support 'some typechecking details' that
> aren't entirely trivial to support that same extension is an awful big ask!
> OutsideIn(X) is a big paper to read, let alone implement, and the only
> compiler to even try handling (~) today is GHC.
>
> -Edward
>
> On Fri, Aug 5, 2016 at 2:15 PM, Ryan Scott <[hidden email]> wrote:
>>
>> Hi David,
>>
>> > Could we get a separate LANGUAGE pragma just for equality constraints?
>>
>> I think we should, and I don't think we'd even need to introduce a new
>> pragma, since there's already a perfectly good one: -XTypeOperators!
>> After all, there's nothing really that special about (~) other than
>> some typechecking details. A fix to Trac #9194 [1] would give us this.
>>
>> Ryan S.
>> -----
>> [1] https://ghc.haskell.org/trac/ghc/ticket/9194
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
_______________________________________________
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: Can we offer ~ without GADTs or type families?

Adam Gundry-2
In reply to this post by David Feuer
On 05/08/16 19:08, David Feuer wrote:
> It seems to me that equality constraints could potentially be supported
> by an implementation with neither GADTs nor type families. Type families
> don't really seem to have much to do with it, and GADTs are strictly
> heavier (GADTs ~= ExistentialQuantification + TypeEquality).
>
> Could we get a separate LANGUAGE pragma just for equality constraints?

I suggested this in #10431 [1], where there is some discussion of the
implications. I still think it is a good idea, and I don't think the
implementation would be very difficult.

All the best,

Adam

[1] https://ghc.haskell.org/trac/ghc/ticket/10431


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
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: Can we offer ~ without GADTs or type families?

crockeea
As a user who frequently uses ~, but doesn't need the rest of GADTs or TypeFamilies, I'd really like to see a TypeEqualities extension!

Eric

On Fri, Aug 5, 2016 at 3:27 PM, Adam Gundry <[hidden email]> wrote:
On 05/08/16 19:08, David Feuer wrote:
> It seems to me that equality constraints could potentially be supported
> by an implementation with neither GADTs nor type families. Type families
> don't really seem to have much to do with it, and GADTs are strictly
> heavier (GADTs ~= ExistentialQuantification + TypeEquality).
>
> Could we get a separate LANGUAGE pragma just for equality constraints?

I suggested this in #10431 [1], where there is some discussion of the
implications. I still think it is a good idea, and I don't think the
implementation would be very difficult.

All the best,

Adam

[1] https://ghc.haskell.org/trac/ghc/ticket/10431


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


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