<div dir="auto">Hi Dmitriy,</div><div dir="auto"><br></div><div dir="auto">Would you like to re-ask over at the haskell cafe mailing list?</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">Best, Kim-Ee</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Dec 30, 2021 at 9:10 PM Dmitriy Matrosov <<a href="mailto:sgf.dma@gmail.com">sgf.dma@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)">Hi.<br>
<br>
I've tried to write a function to coerce existential value according to type<br>
stored in type-level 'Maybe' (i.e. 'Just or 'Nothing).<br>
<br>
> {-# LANGUAGE DataKinds #-}<br>
> {-# LANGUAGE RankNTypes #-}<br>
> {-# LANGUAGE KindSignatures #-}<br>
> {-# LANGUAGE PolyKinds #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> {-# LANGUAGE GADTs #-}<br>
><br>
> import Data.Kind<br>
> import Data.Proxy<br>
> import Unsafe.Coerce<br>
><br>
> class FromTypeMaybe k where<br>
> type ToType k<br>
> fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)<br>
><br>
> instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where<br>
> type ToType 'Nothing = t<br>
> fromTypeMaybe f _ x = Nothing<br>
><br>
> instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe Type) where<br>
> type ToType ('Just t) = t<br>
> fromTypeMaybe f _ x = Just (f x)<br>
><br>
> data Any where<br>
> Any :: a -> Any<br>
><br>
> unAny :: Any -> t<br>
> unAny (Any x) = unsafeCoerce x<br>
<br>
This works as far as i can see<br>
<br>
*Main> fromTypeMaybe unAny (Proxy @('Just Int)) (Any 3)<br>
Just 3<br>
*Main> fromTypeMaybe unAny (Proxy @'Nothing) undefined<br>
Nothing<br>
<br>
but i don't understand how 'Nothing instance works:<br>
<br>
type kind kind?<br>
vvv vvvvvv vvv<br>
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where<br>
type ToType 'Nothing = t<br>
^^^<br>
type<br>
<br>
(in case alignment breaks: variable 't' in forall is type-variable with kind<br>
'Type', but in "Maybe t" in instance head it's used as kind-variable. And then<br>
in associated type-family the same variable 't' is used as type-variable<br>
again).<br>
<br>
If i try to write "'Nothing"'s kind as 'Maybe Type' (in the same manner as<br>
'Just has)<br>
<br>
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe Type) where<br>
<br>
i get an error:<br>
<br>
1.lhs:21:3: error:<br>
• Type variable ‘t’ is mentioned in the RHS,<br>
but not bound on the LHS of the family instance<br>
• In the type instance declaration for ‘ToType’<br>
In the instance declaration for<br>
‘FromTypeMaybe ('Nothing :: Maybe Type)’<br>
|<br>
21 | > instance forall (t :: Type). FromTypeMaybe ('Nothing ::<br>
Maybe Type) where<br>
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...<br>
<br>
Well, i'm not sure, that understand why 'forall' in instance head may not be<br>
used as family's LHS, but.. that's probably ok. On the other hand, if i try<br>
to write 'Just instance using type-variable 't' as kind-variable (in the same<br>
manner as 'Nothing has):<br>
<br>
instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where<br>
<br>
i get an error too:<br>
<br>
1.lhs:25:47: error:<br>
• Expected kind ‘Maybe t’, but ‘'Just t’ has kind ‘Maybe *’<br>
• In the first argument of ‘FromTypeMaybe’, namely<br>
‘('Just t :: Maybe t)’<br>
In the instance declaration for<br>
‘FromTypeMaybe ('Just t :: Maybe t)’<br>
|<br>
25 | > instance forall (t :: Type). FromTypeMaybe ('Just t :: Maybe t) where<br>
<br>
Well, that's also probably expected, because though i've declared<br>
type-variable 't' with kind 'Type' in forall, due to 'DataKinds' extension<br>
type 't' is also promoted to kind 't' and, thus, by using ('Just t :: Maybe t)<br>
i say, that ('Just t) should have kind 'Maybe t', not 'Maybe Type', which it<br>
really has.<br>
<br>
But if that's so, how working 'Nothing instance<br>
<br>
instance forall (t :: Type). FromTypeMaybe ('Nothing :: Maybe t) where<br>
<br>
may work at all? It has the same problem as 'Just instance above:<br>
type-variable 't' is promoted to kind 't' and 'Nothing will have kind 'Maybe<br>
t' instead of 'Maybe Type' ?<br>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
</blockquote></div></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">-- Kim-Ee</div>