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

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 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.