[Haskell-beginners] Coercing existential according to type-level Maybe

[Kim-Ee Yeoh]

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.dma at 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 at 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.html>