[Haskell-cafe] Coercing existential according to type-level Maybe (re-post from h-beginners)

[Richard Eisenberg]

Hi Dmitriy,

Fun stuff here!

- Have you looked at https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Dynamic.html ? That may have the functionality you're looking for. It's quite a bit simpler than the construction you're building, but it might satisfy your eventual use-case.

- GHC does not distinguish between types and kinds, since GHC 8.0. Much literature about Haskell continues to make this distinction, including GHC's own error messages (at some implementation challenge, even). This is because, most of the time, programs don't cross the line between types and kinds, and this distinction can be helpful. However, your code does shuttle ideas back and forth across the line, and so the distinction is harmful. Bottom line here: treat types and kinds as synonyms. The design of Haskell does, internally.

- I think the crux of your question is why (Just t :: Maybe t) fails to type-check. We can see this in the type of Just: Just :: forall (a :: Type). a -> Maybe a. When we write `Just t` (for `t :: Type`), GHC sees `Just @Type t`, supplying the invisible instantiation for the `forall (a :: Type)` argument in Just's type. We can now see that `Just @Type t` will have type `Maybe Type`, just by substituting in Just's type. So saying `Just t :: Maybe t` will be rejected.

- On the other hand, `Nothing :: Maybe t` is fine. We have `Nothing :: forall (a :: Type). Maybe a`, and so `Nothing :: Maybe t` really means `Nothing @t :: Maybe t`, and all is well.

I worry that there is more in your email that I haven't answered here. If so, please write back!

Richard

> On Dec 30, 2021, at 9:50 AM, Dmitriy Matrosov <sgf.dma at gmail.com> wrote:
> 
> (as suggested, i'm re-asking here)
> 
> 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
>> instance forall (t :: Type). FromTypeMaybe ('Nothing @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 another question.  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' ?
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.