[Haskell-cafe] Promoted data types
coot at coot.me
coot at coot.me
Mon May 3 19:59:05 UTC 2021
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>
More information about the Haskell-Cafe
mailing list