Kind equalities

[Simon Peyton Jones]

Richard

What’s your ETA on the kind-equality stuff?  We wondered in today’s call.  We 
want to make an RC next week.

Simon
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kind equalities

[Richard Eisenberg]

I'm on track for that. Did a bunch of performance-related debugging over the 
weekend, and I can observe nice improvements. Just checking those fixes now. If 
the results are acceptable, I have to double-check testsuite wibbles and then 
I'll rebase, validate, and push.

Richard

On Dec 7, 2015, at 10:26 AM, Simon Peyton Jones  wrote:

> Richard
>  
> What’s your ETA on the kind-equality stuff?  We wondered in today’s call.  We 
> want to make an RC next week.
>  
> Simon

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kind equalities update

[Alexander Berntsen]

-BEGIN PGP SIGNED MESSAGE-
Hash: SHA512

On 14/10/15 10:31, Simon Peyton Jones wrote:
> FWIW I think I'm in favour of "Type" (over "type") too.
I am as well.

In fact, Type > * > type > *, where the first * is the one we have
today, and the second * is the wildcard. That should underline how
much I dislike "type". ;)
- -- 
Alexander
alexan...@plaimi.net
https://secure.plaimi.net/~alexander
-BEGIN PGP SIGNATURE-
Version: GnuPG v2

iQIcBAEBCgAGBQJWHh2SAAoJENQqWdRUGk8BY9QQAK+Hf3MWYNi+4ujUV5aPe9FH
uGp3OWBVmkRpy8Ry6fzUnypkpcZzCGwM+8SEB5g/nylXUPXDB0MC7wYgMv6zgml3
Eom0avIWx5EO1h5k/eJUp1MND/LKboVADYaOJdL35d32BkJViiLujhlZaNjBurnj
guLSm5eFGHPf0zlovUDUzzBBpYTH9nxgT7K4DPH2pHu5a/gyr7GKP/aZa+1LoEm8
Zt31v7m6U3LocYt71ZxYHFrrIuzR8PPK2SmqEruNes2+UAvVuuqybp/caQOfJZ93
9iNqQueYRqG4eMXYQgbHza1GYI8N7I7IXjpg16xkrglyhYRH18eDrsTHesNzn2Ah
BkLIIIbAja2R0FvhZ3dRxY3g8kavhmNQjAtWLUcumhmXYLDUnIFMCR5p/CqWMAR2
eNgtDUtDqwfBz6jx9B5WRz+YgtaY5uYPHBzlzVl8+VOKRwWyjdUBdTpHPb5EKIYU
PhHqhymejnvwy9yCPsvOMBVgVNjuxVvntcnqI3ZhhlqOc2D6F63NQej3E5fJN9eg
QTFD2cY8+7DQ1NbzRQP0IsEQ566r3KkPzaV8dJ76DTbBgjtZ6lBpSR7z1U3e+ySd
FqmtDEuoVNb1iGvbLWdBgH0A6E2wXxV10zMsAax65I3Pkskmz1qBIPptgcRCvfin
iEi1wmEk7/aPE9B6Cq3s
=E+WD
-END PGP SIGNATURE-
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Kind equalities update

[Simon Peyton Jones]

FWIW I think I'm in favour of "Type" (over "type") too.

Simon

From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Richard 
Eisenberg
Sent: 14 October 2015 03:27
To: ghc-devs@haskell.org Devs
Subject: Re: Kind equalities update

This feedback is very helpful. And no direction here is more work than any 
other -- I haven't implemented this piece yet.

I'm not tied, at all, to `type`. I just personally think it's the best option. 
But it's completely a stylistic choice, and I'm quite happy to go with the 
majority on this point. As a counter-argument to the "hard to parse for humans" 
point: any syntax-highlighter for Haskell will color `type` differently, 
significantly easing this problem. And I'll also say that * is very confusing 
to beginners, in my experience: lots of people (myself included at one point) 
think that * is somehow a wildcard.

If we do adopt Type, there's no reason we have to reserve it. It could be 
exported from, say, Data.Kind (along with Constraint). Once (which may be 
never) we remove *, users who want kind annotations will just have to import a 
module. So, using Type would be just as backward-compatible as any other 
decision. Because we'll have kind synonyms, a large codebase could even type 
`type TYPE = Data.Kind.Type` or something to avoid name clashes. (This trick 
would work with any solution... even just leaving * alone!)

To be very clear: I'm *not* proposing removing * anytime soon! Following the 
decision to aim for a 3-year window of warning-free code, we couldn't remove * 
until there have been 2 years of having an alternative. And even then, it's not 
clear to me that it's worth the trouble. Maybe we'll just deprecate it with no 
intent to remove. But we can wait to have that debate later.

Again, thanks for the feedback!
Richard

On Oct 13, 2015, at 9:09 PM, Christopher Allen 
<c...@www.bitemyapp.com<mailto:c...@www.bitemyapp.com>> wrote:


My opinion may not count for a lot from a compiler engineering perspective, but 
I can say with a fair bit of confidence that violating the "capitalized -> 
concrete constructor, lowercase -> variable" convention for types would be 
_very_ surprising to learners and users. I don't think it's a petty issue at 
all. This isn't a mistake we have to live with, even if it's regrettable that 
it's more work for Richard.

>(Wadler's Law strikes again!)

Apologies for my contributions on this front, didn't disagree with anything 
else and wanted to bolster Austin's concerns here.

On Tue, Oct 13, 2015 at 7:37 PM, Austin Seipp 
<aus...@well-typed.com<mailto:aus...@well-typed.com>> wrote:
Hey Richard,

Thanks a lot. I'm very eager to see this land ASAP! It's exciting. But...

Looking at the page, I really, really am still not a fan of using
'type' in place of *, and I still think (as I mentioned on Reddit I
believe) that 'Type' is the best choice for this. I mentioned this to
Simon earlier, and I kind of hate to make even more work for you, but
my basic reasoning is:

  - '*' is not a good choice because it's a lexical wart. But in terms
of 'theory', the statement '* :: *' is completely OK, or 'type ::
type' or or 'U :: U' or 'Type :: Type'. That is, the reason star is
bad is because it's a lexical problem that leads to weird ambiguous
parsing, not that it's necessarily confusing or using any particular
word I think.

  - 'type' is not a good choice, because while in theory any name is
kind of arbitrary, it's very confusing for Haskell IMO - we have
_chosen_ the distinction between type variables and type constructors
through the use of capitalization. I think it's a bit strange to say
'*' or what have you has type 'type' yet 'type' is not an actual
variable, nor a keyword in a meaningful sense, but an actual type on
its own. Yet 0-arity type constructors of all sorts (like Int or Bool)
have this lexical capitalization! That is, 'type' isn't confusing
because it's a lexical wart, or has bad parsing - but because it
violates how we syntactically distinguish type variables from
constructors of types.

  - (Correct if I'm wrong) As far as I understand, 'Type' doesn't need
to be reserved unless -XTypeInType is enabled, correct? I think it is
fairly reasonable to say that extensions may take up parts of your
namespace should you enable them - for example, -XStaticPointers
steals the term 'static' for itself, which I think is OK!

  - As far as code breakage goes, I think the prior point makes the
outright breakage minimal-to-none if true, which is great. Even GHC
uses the name `Type`, but we wouldn't even be able to use -XTypeInType
for another few years at best! So we have plenty of time to address
that when we want to use it...

I suppose #2 is a little 'feels-y', since 'violating' how we expect to
read Haskell is maybe subjective. But I figure I might as well make a
last ditch effort at the cost of a little stirring.

I think that mostly sums it up. I

Re: Kind equalities update

[Richard Eisenberg]

Bah. I give in. :)

`Type` it shall be. (And * will stay. But please use `Type`!)

On Oct 14, 2015, at 5:17 AM, Alexander Berntsen  wrote:

> -BEGIN PGP SIGNED MESSAGE-
> Hash: SHA512
> 
> On 14/10/15 10:31, Simon Peyton Jones wrote:
>> FWIW I think I'm in favour of "Type" (over "type") too.
> I am as well.
> 
> In fact, Type > * > type > *, where the first * is the one we have
> today, and the second * is the wildcard. That should underline how
> much I dislike "type". ;)
> - -- 
> Alexander
> alexan...@plaimi.net
> https://secure.plaimi.net/~alexander
> -BEGIN PGP SIGNATURE-
> Version: GnuPG v2
> 
> iQIcBAEBCgAGBQJWHh2SAAoJENQqWdRUGk8BY9QQAK+Hf3MWYNi+4ujUV5aPe9FH
> uGp3OWBVmkRpy8Ry6fzUnypkpcZzCGwM+8SEB5g/nylXUPXDB0MC7wYgMv6zgml3
> Eom0avIWx5EO1h5k/eJUp1MND/LKboVADYaOJdL35d32BkJViiLujhlZaNjBurnj
> guLSm5eFGHPf0zlovUDUzzBBpYTH9nxgT7K4DPH2pHu5a/gyr7GKP/aZa+1LoEm8
> Zt31v7m6U3LocYt71ZxYHFrrIuzR8PPK2SmqEruNes2+UAvVuuqybp/caQOfJZ93
> 9iNqQueYRqG4eMXYQgbHza1GYI8N7I7IXjpg16xkrglyhYRH18eDrsTHesNzn2Ah
> BkLIIIbAja2R0FvhZ3dRxY3g8kavhmNQjAtWLUcumhmXYLDUnIFMCR5p/CqWMAR2
> eNgtDUtDqwfBz6jx9B5WRz+YgtaY5uYPHBzlzVl8+VOKRwWyjdUBdTpHPb5EKIYU
> PhHqhymejnvwy9yCPsvOMBVgVNjuxVvntcnqI3ZhhlqOc2D6F63NQej3E5fJN9eg
> QTFD2cY8+7DQ1NbzRQP0IsEQ566r3KkPzaV8dJ76DTbBgjtZ6lBpSR7z1U3e+ySd
> FqmtDEuoVNb1iGvbLWdBgH0A6E2wXxV10zMsAax65I3Pkskmz1qBIPptgcRCvfin
> iEi1wmEk7/aPE9B6Cq3s
> =E+WD
> -END PGP SIGNATURE-
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kind equalities update

[Richard Eisenberg]

ust got to this point and decided to shout. (Wadler's Law strikes
> again!)
> 
> 
> On Tue, Oct 13, 2015 at 12:32 PM, Richard Eisenberg <e...@cis.upenn.edu> 
> wrote:
> > Hi devs,
> >
> > In a chat with Simon this morning about kind equalities, he expressed that 
> > you all might want to know about the plans for kind equalities in 8.0.
> >
> > The wiki page both for user-facing changes and for implementation notes is 
> > here: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1
> > It is my intent that all user-facing changes mentioned there will be 
> > available in 8.0. I am hard at work getting my branch ready to merge, and 
> > hope to do so mid-November.
> >
> > Note: this is almost fully backward-compatible. Here are some areas where 
> > there are known incompatibilities:
> > - Template Haskell will have to be updated. But there's a raft of changes 
> > there, anyway.
> > - GHC will do a more careful job of checking for termination of instances 
> > regarding the use of kind variables. This may require new 
> > UndecidableInstances declarations. But the fact that these definitions 
> > (like `instance (C a, C b) => C (a b)` for a polykinded C) were accepted 
> > previously could be called a bug.
> >
> > That's actually all I know of so far.
> >
> > You can take kind equalities for a spin at github.com/goldfirere/ghc, on 
> > the "nokinds" branch. Note that this hasn't been merged with `master` since 
> > December of last year, so expect a little strange behavior compared with 
> > 7.10. These wrinkles will get smoothed out, of course.
> >
> > Richard
> > ___
> > ghc-devs mailing list
> > ghc-devs@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
> 
> 
> 
> --
> Regards,
> 
> Austin Seipp, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 
> 
> 
> -- 
> Chris Allen
> Currently working on http://haskellbook.com

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Kind equalities update

[Richard Eisenberg]

Hi devs,

In a chat with Simon this morning about kind equalities, he expressed that you 
all might want to know about the plans for kind equalities in 8.0.

The wiki page both for user-facing changes and for implementation notes is 
here: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1
It is my intent that all user-facing changes mentioned there will be available 
in 8.0. I am hard at work getting my branch ready to merge, and hope to do so 
mid-November.

Note: this is almost fully backward-compatible. Here are some areas where there 
are known incompatibilities:
- Template Haskell will have to be updated. But there's a raft of changes 
there, anyway.
- GHC will do a more careful job of checking for termination of instances 
regarding the use of kind variables. This may require new UndecidableInstances 
declarations. But the fact that these definitions (like `instance (C a, C b) => 
C (a b)` for a polykinded C) were accepted previously could be called a bug.

That's actually all I know of so far.

You can take kind equalities for a spin at github.com/goldfirere/ghc, on the 
"nokinds" branch. Note that this hasn't been merged with `master` since 
December of last year, so expect a little strange behavior compared with 7.10. 
These wrinkles will get smoothed out, of course.

Richard
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kind equalities update

[Austin Seipp]

Hey Richard,

Thanks a lot. I'm very eager to see this land ASAP! It's exciting. But...

Looking at the page, I really, really am still not a fan of using
'type' in place of *, and I still think (as I mentioned on Reddit I
believe) that 'Type' is the best choice for this. I mentioned this to
Simon earlier, and I kind of hate to make even more work for you, but
my basic reasoning is:

  - '*' is not a good choice because it's a lexical wart. But in terms
of 'theory', the statement '* :: *' is completely OK, or 'type ::
type' or or 'U :: U' or 'Type :: Type'. That is, the reason star is
bad is because it's a lexical problem that leads to weird ambiguous
parsing, not that it's necessarily confusing or using any particular
word I think.

  - 'type' is not a good choice, because while in theory any name is
kind of arbitrary, it's very confusing for Haskell IMO - we have
_chosen_ the distinction between type variables and type constructors
through the use of capitalization. I think it's a bit strange to say
'*' or what have you has type 'type' yet 'type' is not an actual
variable, nor a keyword in a meaningful sense, but an actual type on
its own. Yet 0-arity type constructors of all sorts (like Int or Bool)
have this lexical capitalization! That is, 'type' isn't confusing
because it's a lexical wart, or has bad parsing - but because it
violates how we syntactically distinguish type variables from
constructors of types.

  - (Correct if I'm wrong) As far as I understand, 'Type' doesn't need
to be reserved unless -XTypeInType is enabled, correct? I think it is
fairly reasonable to say that extensions may take up parts of your
namespace should you enable them - for example, -XStaticPointers
steals the term 'static' for itself, which I think is OK!

  - As far as code breakage goes, I think the prior point makes the
outright breakage minimal-to-none if true, which is great. Even GHC
uses the name `Type`, but we wouldn't even be able to use -XTypeInType
for another few years at best! So we have plenty of time to address
that when we want to use it...

I suppose #2 is a little 'feels-y', since 'violating' how we expect to
read Haskell is maybe subjective. But I figure I might as well make a
last ditch effort at the cost of a little stirring.

I think that mostly sums it up. I'm still reading over the full page,
I just got to this point and decided to shout. (Wadler's Law strikes
again!)


On Tue, Oct 13, 2015 at 12:32 PM, Richard Eisenberg <e...@cis.upenn.edu> wrote:
> Hi devs,
>
> In a chat with Simon this morning about kind equalities, he expressed that 
> you all might want to know about the plans for kind equalities in 8.0.
>
> The wiki page both for user-facing changes and for implementation notes is 
> here: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1
> It is my intent that all user-facing changes mentioned there will be 
> available in 8.0. I am hard at work getting my branch ready to merge, and 
> hope to do so mid-November.
>
> Note: this is almost fully backward-compatible. Here are some areas where 
> there are known incompatibilities:
> - Template Haskell will have to be updated. But there's a raft of changes 
> there, anyway.
> - GHC will do a more careful job of checking for termination of instances 
> regarding the use of kind variables. This may require new 
> UndecidableInstances declarations. But the fact that these definitions (like 
> `instance (C a, C b) => C (a b)` for a polykinded C) were accepted previously 
> could be called a bug.
>
> That's actually all I know of so far.
>
> You can take kind equalities for a spin at github.com/goldfirere/ghc, on the 
> "nokinds" branch. Note that this hasn't been merged with `master` since 
> December of last year, so expect a little strange behavior compared with 
> 7.10. These wrinkles will get smoothed out, of course.
>
> Richard
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>



-- 
Regards,

Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kind equalities update

[Christopher Allen]

My opinion may not count for a lot from a compiler engineering perspective,
but I can say with a fair bit of confidence that violating the "capitalized
-> concrete constructor, lowercase -> variable" convention for types would
be _very_ surprising to learners and users. I don't think it's a petty
issue at all. This isn't a mistake we have to live with, even if it's
regrettable that it's more work for Richard.

>(Wadler's Law strikes again!)

Apologies for my contributions on this front, didn't disagree with anything
else and wanted to bolster Austin's concerns here.

On Tue, Oct 13, 2015 at 7:37 PM, Austin Seipp <aus...@well-typed.com> wrote:

> Hey Richard,
>
> Thanks a lot. I'm very eager to see this land ASAP! It's exciting. But...
>
> Looking at the page, I really, really am still not a fan of using
> 'type' in place of *, and I still think (as I mentioned on Reddit I
> believe) that 'Type' is the best choice for this. I mentioned this to
> Simon earlier, and I kind of hate to make even more work for you, but
> my basic reasoning is:
>
>   - '*' is not a good choice because it's a lexical wart. But in terms
> of 'theory', the statement '* :: *' is completely OK, or 'type ::
> type' or or 'U :: U' or 'Type :: Type'. That is, the reason star is
> bad is because it's a lexical problem that leads to weird ambiguous
> parsing, not that it's necessarily confusing or using any particular
> word I think.
>
>   - 'type' is not a good choice, because while in theory any name is
> kind of arbitrary, it's very confusing for Haskell IMO - we have
> _chosen_ the distinction between type variables and type constructors
> through the use of capitalization. I think it's a bit strange to say
> '*' or what have you has type 'type' yet 'type' is not an actual
> variable, nor a keyword in a meaningful sense, but an actual type on
> its own. Yet 0-arity type constructors of all sorts (like Int or Bool)
> have this lexical capitalization! That is, 'type' isn't confusing
> because it's a lexical wart, or has bad parsing - but because it
> violates how we syntactically distinguish type variables from
> constructors of types.
>
>   - (Correct if I'm wrong) As far as I understand, 'Type' doesn't need
> to be reserved unless -XTypeInType is enabled, correct? I think it is
> fairly reasonable to say that extensions may take up parts of your
> namespace should you enable them - for example, -XStaticPointers
> steals the term 'static' for itself, which I think is OK!
>
>   - As far as code breakage goes, I think the prior point makes the
> outright breakage minimal-to-none if true, which is great. Even GHC
> uses the name `Type`, but we wouldn't even be able to use -XTypeInType
> for another few years at best! So we have plenty of time to address
> that when we want to use it...
>
> I suppose #2 is a little 'feels-y', since 'violating' how we expect to
> read Haskell is maybe subjective. But I figure I might as well make a
> last ditch effort at the cost of a little stirring.
>
> I think that mostly sums it up. I'm still reading over the full page,
> I just got to this point and decided to shout. (Wadler's Law strikes
> again!)
>
>
> On Tue, Oct 13, 2015 at 12:32 PM, Richard Eisenberg <e...@cis.upenn.edu>
> wrote:
> > Hi devs,
> >
> > In a chat with Simon this morning about kind equalities, he expressed
> that you all might want to know about the plans for kind equalities in 8.0.
> >
> > The wiki page both for user-facing changes and for implementation notes
> is here: https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1
> > It is my intent that all user-facing changes mentioned there will be
> available in 8.0. I am hard at work getting my branch ready to merge, and
> hope to do so mid-November.
> >
> > Note: this is almost fully backward-compatible. Here are some areas
> where there are known incompatibilities:
> > - Template Haskell will have to be updated. But there's a raft of
> changes there, anyway.
> > - GHC will do a more careful job of checking for termination of
> instances regarding the use of kind variables. This may require new
> UndecidableInstances declarations. But the fact that these definitions
> (like `instance (C a, C b) => C (a b)` for a polykinded C) were accepted
> previously could be called a bug.
> >
> > That's actually all I know of so far.
> >
> > You can take kind equalities for a spin at github.com/goldfirere/ghc,
> on the "nokinds" branch. Note that this hasn't been merged with `master`
> since December of last year, so expect a little strange behavior compared
> with 7.10. These wrinkles will get smoothed out, of course.
> >
> > Richard
> > 

Re: would support for kind equalities enable the following example?

[Richard Eisenberg]

My question is: why do you want Eff to be a GADT? It's true that GADTs do not 
promote (currently), which is why your first example doesn't work. (It's not to 
do with kinds, exactly, but GADTs.) But, I don't quite see a reason for having 
a GADT there -- generally, when a GADT is really useful, no amount of 
defunctionalization will be a substitute.

GHC ticket #7961 is a place to make noise about this. My (with co-authors 
Stephanie Weirich and Justin Hsu) ICFP paper from last year (System FC with 
Explicit Kind Equality) is part of the solution, and I was planning on 
submitting the other part of the solution (type inference!) for ICFP this year. 
Alas, that won't happen, but I believe I should be able to pull it together for 
the POPL deadline (July). So, there's somewhat slow but somewhat steady work in 
this direction, and I'm confident something will make its way into GHC before 
too long.

Richard

On Feb 24, 2014, at 11:28 PM, Carter Schonwald carter.schonw...@gmail.com 
wrote:

 Hey all, 
 
 I've a use case in my code where It looks like it might be an example of 
 something that won't compile until we have type level GADTs
 
 I'm essentially writing a vector api that 
 allows certain args to be mutable, pure or dont care. (dont care = that 
 they're treated as being immutable). I'm using GADTs to model this. (using 
 GADTs rather than type classes partly because I want to make sure type 
 inference works out nicely, and partly to see how far i can go while not 
 adding any new type classes)
 
 data Eff :: * - * where
 Pure :: Eff () 
 Mut :: s - Eff s 
  
 data EVector  :: * - * - * where 
 PureVector :: S.Vector el  - EVector Pure el 
 MutVector :: SM.MVector s el - EVector (Mut s) el  
 
 the above doesn't work because DataKinds only works at kind * currently,
 however i can defunctionalize it to the following (while making it a tad less 
 pretty)
 and it then works
 
 data Eff = Pure | Mut 
 
 data EVector  :: Eff - * - * - * where 
 PureVector :: S.Vector el  - EVector Pure () el 
 MutVector :: SM.MVector s el - EVector Mut s  el   
 
 
 am i correct in thinking that the first example *should* be possible once we 
 have fancier kind machinery (kind equalities and type level GADTs?)? I 
 suspect I'll be hitting *A LOT* more examples like the above, and if theres 
 any ways I can help push this along on the research or engineering side, I 
 please tell me :) 
 
 thanks!
 -Carter
 
 

___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

Re: would support for kind equalities enable the following example?

[Carter Schonwald]

IN this case i *DO* want the GADT. (but i can't express it)

The reason is simple: one type parameter makes for a less complex API to
educate others about than 2 type parameters. And likewise for 3 vs 4. Etc
etc. Its a human factors thing :)

I do agree in this case that my defunctionalized type is equivalent in
type safety, and i'm happy to use it for now.




On Tue, Feb 25, 2014 at 6:50 AM, Richard Eisenberg e...@cis.upenn.eduwrote:

 My question is: why do you want Eff to be a GADT? It's true that GADTs do
 not promote (currently), which is why your first example doesn't work.
 (It's not to do with kinds, exactly, but GADTs.) But, I don't quite see a
 reason for having a GADT there -- generally, when a GADT is really useful,
 no amount of defunctionalization will be a substitute.

 GHC ticket #7961 is a place to make noise about this. My (with co-authors
 Stephanie Weirich and Justin Hsu) ICFP paper from last year (System FC
 with Explicit Kind Equality) is part of the solution, and I was planning
 on submitting the other part of the solution (type inference!) for ICFP
 this year. Alas, that won't happen, but I believe I should be able to pull
 it together for the POPL deadline (July). So, there's somewhat slow but
 somewhat steady work in this direction, and I'm confident something will
 make its way into GHC before too long.

 Richard

 On Feb 24, 2014, at 11:28 PM, Carter Schonwald carter.schonw...@gmail.com
 wrote:

  Hey all,
 
  I've a use case in my code where It looks like it might be an example of
 something that won't compile until we have type level GADTs
 
  I'm essentially writing a vector api that
  allows certain args to be mutable, pure or dont care. (dont care =
 that they're treated as being immutable). I'm using GADTs to model this.
 (using GADTs rather than type classes partly because I want to make sure
 type inference works out nicely, and partly to see how far i can go while
 not adding any new type classes)
 
  data Eff :: * - * where
  Pure :: Eff ()
  Mut :: s - Eff s
 
  data EVector  :: * - * - * where
  PureVector :: S.Vector el  - EVector Pure el
  MutVector :: SM.MVector s el - EVector (Mut s) el
 
  the above doesn't work because DataKinds only works at kind * currently,
  however i can defunctionalize it to the following (while making it a tad
 less pretty)
  and it then works
 
  data Eff = Pure | Mut
 
  data EVector  :: Eff - * - * - * where
  PureVector :: S.Vector el  - EVector Pure () el
  MutVector :: SM.MVector s el - EVector Mut s  el
 
 
  am i correct in thinking that the first example *should* be possible
 once we have fancier kind machinery (kind equalities and type level
 GADTs?)? I suspect I'll be hitting *A LOT* more examples like the above,
 and if theres any ways I can help push this along on the research or
 engineering side, I please tell me :)
 
  thanks!
  -Carter
 
 


___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

Re: would support for kind equalities enable the following example?

[Carter Schonwald]

Reid Just helped me whack out a solution, it involve something i didn't
even know was possible in haskell

data Eff :: *- *  where
Pure :: Eff s
Mut :: s - Eff s

data EVector :: Eff * - * - *  where
PureVector :: S.Vector el  - EVector Pure el
MutVector :: SM.MVector s e - EVector (Mut s) el

(the surprising thing was the Eff *, i didn't know we could do that!)
this type checks, but it can be made simpler still!

data Eff s where
Pure :: Eff s
Mut :: s - Eff s

data EVector s el  where
PureVector :: S.Vector el  - EVector Pure el
MutVector :: SM.MVector s e - EVector (Mut s) el

:)

that said, I do have some more interesting stuff in the works where I hope
to make use of kind level gadts, so i look forward to finding out how that
shakes out!

-Carter




On Tue, Feb 25, 2014 at 10:23 PM, Carter Schonwald 
carter.schonw...@gmail.com wrote:

 IN this case i *DO* want the GADT. (but i can't express it)

 The reason is simple: one type parameter makes for a less complex API to
 educate others about than 2 type parameters. And likewise for 3 vs 4. Etc
 etc. Its a human factors thing :)

 I do agree in this case that my defunctionalized type is equivalent in
 type safety, and i'm happy to use it for now.




 On Tue, Feb 25, 2014 at 6:50 AM, Richard Eisenberg e...@cis.upenn.eduwrote:

 My question is: why do you want Eff to be a GADT? It's true that GADTs do
 not promote (currently), which is why your first example doesn't work.
 (It's not to do with kinds, exactly, but GADTs.) But, I don't quite see a
 reason for having a GADT there -- generally, when a GADT is really useful,
 no amount of defunctionalization will be a substitute.

 GHC ticket #7961 is a place to make noise about this. My (with co-authors
 Stephanie Weirich and Justin Hsu) ICFP paper from last year (System FC
 with Explicit Kind Equality) is part of the solution, and I was planning
 on submitting the other part of the solution (type inference!) for ICFP
 this year. Alas, that won't happen, but I believe I should be able to pull
 it together for the POPL deadline (July). So, there's somewhat slow but
 somewhat steady work in this direction, and I'm confident something will
 make its way into GHC before too long.

 Richard

 On Feb 24, 2014, at 11:28 PM, Carter Schonwald 
 carter.schonw...@gmail.com wrote:

  Hey all,
 
  I've a use case in my code where It looks like it might be an example
 of something that won't compile until we have type level GADTs
 
  I'm essentially writing a vector api that
  allows certain args to be mutable, pure or dont care. (dont care =
 that they're treated as being immutable). I'm using GADTs to model this.
 (using GADTs rather than type classes partly because I want to make sure
 type inference works out nicely, and partly to see how far i can go while
 not adding any new type classes)
 
  data Eff :: * - * where
  Pure :: Eff ()
  Mut :: s - Eff s
 
  data EVector  :: * - * - * where
  PureVector :: S.Vector el  - EVector Pure el
  MutVector :: SM.MVector s el - EVector (Mut s) el
 
  the above doesn't work because DataKinds only works at kind * currently,
  however i can defunctionalize it to the following (while making it a
 tad less pretty)
  and it then works
 
  data Eff = Pure | Mut
 
  data EVector  :: Eff - * - * - * where
  PureVector :: S.Vector el  - EVector Pure () el
  MutVector :: SM.MVector s el - EVector Mut s  el
 
 
  am i correct in thinking that the first example *should* be possible
 once we have fancier kind machinery (kind equalities and type level
 GADTs?)? I suspect I'll be hitting *A LOT* more examples like the above,
 and if theres any ways I can help push this along on the research or
 engineering side, I please tell me :)
 
  thanks!
  -Carter
 
 



___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

would support for kind equalities enable the following example?

[Carter Schonwald]

Hey all,

I've a use case in my code where It looks like it might be an example of
something that won't compile until we have type level GADTs

I'm essentially writing a vector api that
allows certain args to be mutable, pure or dont care. (dont care = that
they're treated as being immutable). I'm using GADTs to model this. (using
GADTs rather than type classes partly because I want to make sure type
inference works out nicely, and partly to see how far i can go while not
adding any new type classes)

data Eff :: * - * where
Pure :: Eff ()
Mut :: s - Eff s

data EVector  :: * - * - * where
PureVector :: S.Vector el  - EVector Pure el
MutVector :: SM.MVector s el - EVector (Mut s) el

the above doesn't work because DataKinds only works at kind * currently,
however i can defunctionalize it to the following (while making it a tad
less pretty)
and it then works

data Eff = Pure | Mut

data EVector  :: Eff - * - * - * where
PureVector :: S.Vector el  - EVector Pure () el
MutVector :: SM.MVector s el - EVector Mut s  el


am i correct in thinking that the first example *should* be possible once
we have fancier kind machinery (kind equalities and type level GADTs?)? I
suspect I'll be hitting *A LOT* more examples like the above, and if theres
any ways I can help push this along on the research or engineering side, I
please tell me :)

thanks!
-Carter
___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

Re: would support for kind equalities enable the following example?

[Carter Schonwald]

also Ive not been able to find any tickets on Trac for heres some
motiviating example for higher kinded data kinds, happy to great a feature
request ticket motivated by this code if there sin't one :)


On Mon, Feb 24, 2014 at 11:28 PM, Carter Schonwald 
carter.schonw...@gmail.com wrote:

 Hey all,

 I've a use case in my code where It looks like it might be an example of
 something that won't compile until we have type level GADTs

 I'm essentially writing a vector api that
 allows certain args to be mutable, pure or dont care. (dont care = that
 they're treated as being immutable). I'm using GADTs to model this. (using
 GADTs rather than type classes partly because I want to make sure type
 inference works out nicely, and partly to see how far i can go while not
 adding any new type classes)

 data Eff :: * - * where
 Pure :: Eff ()
 Mut :: s - Eff s

 data EVector  :: * - * - * where
 PureVector :: S.Vector el  - EVector Pure el
 MutVector :: SM.MVector s el - EVector (Mut s) el

 the above doesn't work because DataKinds only works at kind * currently,
 however i can defunctionalize it to the following (while making it a tad
 less pretty)
 and it then works

 data Eff = Pure | Mut

 data EVector  :: Eff - * - * - * where
 PureVector :: S.Vector el  - EVector Pure () el
 MutVector :: SM.MVector s el - EVector Mut s  el


 am i correct in thinking that the first example *should* be possible once
 we have fancier kind machinery (kind equalities and type level GADTs?)? I
 suspect I'll be hitting *A LOT* more examples like the above, and if theres
 any ways I can help push this along on the research or engineering side, I
 please tell me :)

 thanks!
 -Carter



___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs