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 <eir at 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 at 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/