[Haskell-cafe] Promoted data types

[coot at coot.me]

Hi David,

My workaround is to use:

> data K a where

>   K0 :: forall a b. b -> K a

The kind `K Bool` contains things like:

> :kind! K0 'True

(K0 'True) :: K Bool

> :kind! K0 'False

(K0 'True) :: K Bool

But also

> :kind! (K0 Int :: K Bool)

(K0 Int :: K Bool) :: K Bool

and I'd like to have a way to not allow to construct such a type.

Oh!, what I just realised is that I can actually achieve what I want by simply declaring:

> data K a where

>   K0 :: forall a. a -> K a

Now the type constructor of a type of kind `K Bool`, must is `K0 'True`, `K0 'False`, or `K0` of some exotic type of kind `Bool`.

Thanks for making me realise that!

Regards,

Marcin

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Monday, May 3rd, 2021 at 22:44, David Feuer <david.feuer at gmail.com> wrote:

> On Mon, May 3, 2021, 8:04 AM <coot at coot.me> wrote:
> 

> > Currently with `DataKind` extension, Haskell allows to promote terms / types to types / kinds.  Currently, one cannot write:
> > 

> > ```
> > 

> > data K a where
> > 

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

> > ```
> 

> I feel like I'm missing something. Suppose `a` is not Type but rather, say, Bool. Then `x` has kind Bool. That is, x is 'True, 'False, or something exotic. K0 @Bool is then a function that takes anything of type 'True or type 'False and gives you something of type K Bool. What I think Richard is getting at is that there isn't anything of type 'True or type 'False, whether at the term level or the type level. These things only exist when `a` is Type (or TYPE rep for some rep :: RuntimeRep). So it's pretty hard to see what you're trying to do.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210503/a6f7a3eb/attachment.html>
-------------- 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/a6f7a3eb/attachment.sig>