[Haskell-cafe] Promoted data types

[coot at coot.me]

Hi Richard,

> type K :: Bool -> Type
> data K b where
>   MkK :: forall a (b :: a). K b

This requests `b` to be of kind `a` for any `a`, and it constraint `b` to by of kind `Bool`, so this cannot be satisfied.

> data K a where
>   K0 :: forall (x :: Type). x -> K Type

There are two levels here:
1. `K a` is a perfectly defined type with a single constructor `K0`.  This is not what I am looking for.
2. `K a` is a kind, `K0 x` for any `x :: Type` is a type of kind `K a`.  This will work only for `x`-es which are of kind `Type`, am interested in `x`-es which are of other kind. So one can proceed with this:

> data K a where
>   K0 :: forall x. x -> K a

The problem here is that the promoted type `K0` is too broad, I'd like to express that I am only interested with `x`-es of kind `a`.

> f :: forall a (b :: a). b -> b

Let's get one step back.  If I couldn't write this

> f :: forall (b :: A). b -> b

I would be forced to write this

> f :: forall b. b -> b

And these are very different (e.g. free theorems).  The concrete 'A', in my case gets generalised and constraint by some type class.  Hence the framework requires

> f :: forall a (b :: a). b -> b

though all the instances provide and use a concrete `a`.


I see your point on error messages, maybe there's a way around it.  Let's say that the author must provide an explicit kind signature, e.g.

> type K0 :: a -> K a
> data K a where
>   K0 :: x -> K a

Such K0 can only be a type; When one would use it at a term level GHC should say: data constructor not in scope (and possibly explain that there is a type of the same name).

Marcin   




‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Monday, May 3rd, 2021 at 19:12, Richard Eisenberg <rae at richarde.dev> wrote:

> Hi Marcin,
> 

> To understand your intent better, what do you think of this:
> 

> > type K :: Bool -> Type
> > 

> > data K b where
> > 

> > MkK :: forall a (b :: a). K b
> 

> Here, the issue isn't whether `a` is `Type`, but whether `a` is `Bool`. Do you think that should be accepted?
> 

> And why restrict this only to GADT type signatures? What about
> 

> > f :: forall a (b :: a). b -> b
> 

> My personal opinion is that we should reject all of these, including your initial suggestion. You're right in that we could infer an extra equality constraint, but I think that would lead to a worse user experience: a definition is accepted only to be rejected at usage sites. It's almost like accepting
> 

> > g x = not x : "hello"
> 

> which could be accepted with an equality constraint (Bool ~ Char). I recognize this last one goes a step further into absurdity, but there is a balance between inferring equality constraints and issuing helpful errors.
> 

> Put another way: Why not write your original datatype as
> 

> > data K a where
> > 

> > K0 :: forall (x :: Type). x -> K Type
> 

> ? That would be accepted and may have your intended meaning.
> 

> > On May 3, 2021, at 12:44 PM, coot at coot.me wrote:
> > 

> > Another missing puzzle is that there's no way to specify that one only wants the promoted types / kinds without the term level part.
> 

> Aha. This one really has been proposed (and accepted!): https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0106-type-data.rst
> 

> There is no one working on an implementation of it yet, though. I'd be happy to advise someone who wanted to dive in!
> 

> Richard
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 509 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/6c7cdff5/attachment.sig>