Proposal: export more from Data.Kind

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

Proposal: export more from Data.Kind

Krzysztof Gogolewski
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

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

Re: Proposal: export more from Data.Kind

chessai .
+1

On Sun, Aug 2, 2020, 9:10 AM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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: Proposal: export more from Data.Kind

David Feuer
In reply to this post by Krzysztof Gogolewski
My impression is that RuntimeRep may not have stabilized all the way yet. There are things that work for LiftedRep and UnliftedRep that want to be polymorphic that way.

On Sun, Aug 2, 2020, 12:10 PM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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: Proposal: export more from Data.Kind

chessai .
I suppose we might want RuntimeRep to stabilise before its inclusion in a non-GHC.* namespace. Open to suggestions on whether that matters - typically people using RuntimeRep know what they're doing, and are small in number, so they could handle the breakage just fine. 



On Sun, Aug 2, 2020, 9:12 AM David Feuer <[hidden email]> wrote:
My impression is that RuntimeRep may not have stabilized all the way yet. There are things that work for LiftedRep and UnliftedRep that want to be polymorphic that way.

On Sun, Aug 2, 2020, 12:10 PM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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

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

Re: Proposal: export more from Data.Kind

Carter Schonwald
In reply to this post by David Feuer
David makes a very good point here. That perhaps they should first stabilize a bit more before being exposed through there 

On Sun, Aug 2, 2020 at 12:12 PM David Feuer <[hidden email]> wrote:
My impression is that RuntimeRep may not have stabilized all the way yet. There are things that work for LiftedRep and UnliftedRep that want to be polymorphic that way.

On Sun, Aug 2, 2020, 12:10 PM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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

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

Re: Proposal: export more from Data.Kind

Richard Eisenberg-5
I'm sympathetic to this proposal, but I don't have a well considered opinion. Instead, I'll present a few facts:

- TYPE, RuntimeRep, and Multiplicity should be allowed in Safe Haskell. You can't do anything untoward with these folks.

- That said, Safe should not imply that linear-types guarantees are in force. At least, not yet. Linear types features cannot cause seg-faults (or other violations of safety expectations).

- RuntimeRep has not yet stabilized. But it is a niche feature, and I wouldn't really expect stabilization here for some time.

Maybe a nice compromise is introducing GHC.Kind that is -XSafe and exports all of these?

Richard

On Aug 3, 2020, at 6:49 AM, Carter Schonwald <[hidden email]> wrote:

David makes a very good point here. That perhaps they should first stabilize a bit more before being exposed through there 

On Sun, Aug 2, 2020 at 12:12 PM David Feuer <[hidden email]> wrote:
My impression is that RuntimeRep may not have stabilized all the way yet. There are things that work for LiftedRep and UnliftedRep that want to be polymorphic that way.

On Sun, Aug 2, 2020, 12:10 PM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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
_______________________________________________
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: Proposal: export more from Data.Kind

Carter Schonwald
That sounds good. Totally all for it. And maybe have that be a one stop shop for kind level stuff like type lits etc?

On Mon, Aug 3, 2020 at 8:29 AM Richard Eisenberg <[hidden email]> wrote:
I'm sympathetic to this proposal, but I don't have a well considered opinion. Instead, I'll present a few facts:

- TYPE, RuntimeRep, and Multiplicity should be allowed in Safe Haskell. You can't do anything untoward with these folks.

- That said, Safe should not imply that linear-types guarantees are in force. At least, not yet. Linear types features cannot cause seg-faults (or other violations of safety expectations).

- RuntimeRep has not yet stabilized. But it is a niche feature, and I wouldn't really expect stabilization here for some time.

Maybe a nice compromise is introducing GHC.Kind that is -XSafe and exports all of these?

Richard

On Aug 3, 2020, at 6:49 AM, Carter Schonwald <[hidden email]> wrote:

David makes a very good point here. That perhaps they should first stabilize a bit more before being exposed through there 

On Sun, Aug 2, 2020 at 12:12 PM David Feuer <[hidden email]> wrote:
My impression is that RuntimeRep may not have stabilized all the way yet. There are things that work for LiftedRep and UnliftedRep that want to be polymorphic that way.

On Sun, Aug 2, 2020, 12:10 PM Krzysztof Gogolewski <[hidden email]> wrote:
Hello,

I'd like to export TYPE, RuntimeRep(..), Multiplicity(..) from Data.Kind.
(Multiplicity is the Linear Haskell type - One and Many.)

Currently you have to import GHC.Exts / GHC.Types which conflicts with
Safe Haskell. I think both levity and linearity polymorphism
should be available under Safe Haskell.

Data.Kind already contains Constraint and Type.

-Krzysztof
_______________________________________________
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
_______________________________________________
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