Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Coercing existential according to type-level Maybe
(Dmitriy Matrosov)
2. Re: Coercing existential according to type-level Maybe
(Kim-Ee Yeoh)
----------------------------------------------------------------------
Message: 1
Date: Thu, 30 Dec 2021 16:10:01 +0300
From: Dmitriy Matrosov <sgf....@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: [Haskell-beginners] Coercing existential according to
type-level Maybe
Message-ID:
<CAFdVUFnXYH=lexjcexmap3ou8aobah+zme4jjoumb4-z+jm...@mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"
Hi.
I've tried to write a function to coerce existential value according to type
stored in type-level 'Maybe' (i.e. 'Just or 'Nothing).
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE GADTs #-}
>
> import Data.Kind
> import Data.Proxy
> import Unsafe.Coerce
>
> class FromTypeMaybe k where
> type ToType k
> fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
>
> instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
> type ToType 'Nothing = t
> fromTypeMaybe f _ x = Nothing
>
> instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe Type) where
> type ToType ('Just t) = t
> fromTypeMaybe f _ x = Just (f x)
>
> data Any where
> Any :: a -> Any
>
> unAny :: Any -> t
> unAny (Any x) = unsafeCoerce x
This works as far as i can see
*Main> fromTypeMaybe unAny (Proxy @('Just Int)) (Any 3)
Just 3
*Main> fromTypeMaybe unAny (Proxy @'Nothing) undefined
Nothing
but i don't understand how 'Nothing instance works:
type kind kind?
vvv vvvvvv vvv
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
type ToType 'Nothing = t
^^^
type
(in case alignment breaks: variable 't' in forall is type-variable with kind
'Type', but in "Maybe t" in instance head it's used as kind-variable. And then
in associated type-family the same variable 't' is used as type-variable
again).
If i try to write "'Nothing"'s kind as 'Maybe Type' (in the same manner as
'Just has)
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe Type) where
i get an error:
1.lhs:21:3: error:
• Type variable ‘t’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the type instance declaration for ‘ToType’
In the instance declaration for
‘FromTypeMaybe ('Nothing :: Maybe Type)’
|
21 | > instance forall (t :: Type). FromTypeMaybe ('Nothing ::
Maybe Type) where
|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Well, i'm not sure, that understand why 'forall' in instance head may not be
used as family's LHS, but.. that's probably ok. On the other hand, if i try
to write 'Just instance using type-variable 't' as kind-variable (in the same
manner as 'Nothing has):
instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where
i get an error too:
1.lhs:25:47: error:
• Expected kind ‘Maybe t’, but ‘'Just t’ has kind ‘Maybe *’
• In the first argument of ‘FromTypeMaybe’, namely
‘('Just t :: Maybe t)’
In the instance declaration for
‘FromTypeMaybe ('Just t :: Maybe t)’
|
25 | > instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where
Well, that's also probably expected, because though i've declared
type-variable 't' with kind 'Type' in forall, due to 'DataKinds' extension
type 't' is also promoted to kind 't' and, thus, by using ('Just t :: Maybe t)
i say, that ('Just t) should have kind 'Maybe t', not 'Maybe Type', which it
really has.
But if that's so, how working 'Nothing instance
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
may work at all? It has the same problem as 'Just instance above:
type-variable 't' is promoted to kind 't' and 'Nothing will have kind 'Maybe
t' instead of 'Maybe Type' ?
------------------------------
Message: 2
Date: Thu, 30 Dec 2021 22:40:47 +0800
From: Kim-Ee Yeoh <k...@atamo.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Coercing existential according to
type-level Maybe
Message-ID:
<capy+zdqchgywvxaug6tkkmldqojqquacqnzxsvn_y6vp8e1...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi Dmitriy,
Would you like to re-ask over at the haskell cafe mailing list?
The beginners list focuses on topics at the level of LYAH. Great for
splaining what a monad is, not so good at coercing existentials via a
type-level Maybe.
Best, Kim-Ee
On Thu, Dec 30, 2021 at 9:10 PM Dmitriy Matrosov <sgf....@gmail.com> wrote:
> Hi.
>
> I've tried to write a function to coerce existential value according to
> type
> stored in type-level 'Maybe' (i.e. 'Just or 'Nothing).
>
> > {-# LANGUAGE DataKinds #-}
> > {-# LANGUAGE RankNTypes #-}
> > {-# LANGUAGE KindSignatures #-}
> > {-# LANGUAGE PolyKinds #-}
> > {-# LANGUAGE TypeFamilies #-}
> > {-# LANGUAGE GADTs #-}
> >
> > import Data.Kind
> > import Data.Proxy
> > import Unsafe.Coerce
> >
> > class FromTypeMaybe k where
> > type ToType k
> > fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
> >
> > instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
> > type ToType 'Nothing = t
> > fromTypeMaybe f _ x = Nothing
> >
> > instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe Type) where
> > type ToType ('Just t) = t
> > fromTypeMaybe f _ x = Just (f x)
> >
> > data Any where
> > Any :: a -> Any
> >
> > unAny :: Any -> t
> > unAny (Any x) = unsafeCoerce x
>
> This works as far as i can see
>
> *Main> fromTypeMaybe unAny (Proxy @('Just Int)) (Any 3)
> Just 3
> *Main> fromTypeMaybe unAny (Proxy @'Nothing) undefined
> Nothing
>
> but i don't understand how 'Nothing instance works:
>
> type kind kind?
> vvv vvvvvv vvv
> instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
> type ToType 'Nothing = t
> ^^^
> type
>
> (in case alignment breaks: variable 't' in forall is type-variable with
> kind
> 'Type', but in "Maybe t" in instance head it's used as kind-variable. And
> then
> in associated type-family the same variable 't' is used as type-variable
> again).
>
> If i try to write "'Nothing"'s kind as 'Maybe Type' (in the same manner as
> 'Just has)
>
> instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe Type)
> where
>
> i get an error:
>
> 1.lhs:21:3: error:
> • Type variable ‘t’ is mentioned in the RHS,
> but not bound on the LHS of the family instance
> • In the type instance declaration for ‘ToType’
> In the instance declaration for
> ‘FromTypeMaybe ('Nothing :: Maybe Type)’
> |
> 21 | > instance forall (t :: Type). FromTypeMaybe ('Nothing ::
> Maybe Type) where
> |
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
>
> Well, i'm not sure, that understand why 'forall' in instance head may not
> be
> used as family's LHS, but.. that's probably ok. On the other hand, if i
> try
> to write 'Just instance using type-variable 't' as kind-variable (in the
> same
> manner as 'Nothing has):
>
> instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where
>
> i get an error too:
>
> 1.lhs:25:47: error:
> • Expected kind ‘Maybe t’, but ‘'Just t’ has kind ‘Maybe *’
> • In the first argument of ‘FromTypeMaybe’, namely
> ‘('Just t :: Maybe t)’
> In the instance declaration for
> ‘FromTypeMaybe ('Just t :: Maybe t)’
> |
> 25 | > instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t)
> where
>
> Well, that's also probably expected, because though i've declared
> type-variable 't' with kind 'Type' in forall, due to 'DataKinds' extension
> type 't' is also promoted to kind 't' and, thus, by using ('Just t ::
> Maybe t)
> i say, that ('Just t) should have kind 'Maybe t', not 'Maybe Type', which
> it
> really has.
>
> But if that's so, how working 'Nothing instance
>
> instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where
>
> may work at all? It has the same problem as 'Just instance above:
> type-variable 't' is promoted to kind 't' and 'Nothing will have kind
> 'Maybe
> t' instead of 'Maybe Type' ?
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
--
-- Kim-Ee
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20211230/54899541/attachment-0001.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 161, Issue 5
*****************************************
