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