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

[Dmitriy Matrosov]

On 1/26/22 10:38 PM, Richard Eisenberg wrote:
> I was at a conference last week and didn't have time to respond... but now that I return to this, I still don't really understand what your question is. Sorry!
> 
> I think this will help: Why invoke GHC.Types.Any at all? What are you hoping to accomplish with GHC.Types.Any?

Well, that's more of a theoretical question. As i wrote earlier, i've fixed
this example (by using type-class definition similar to IsLabel and without
GHC.Types.Any).

But anyway, i try to explain shorter. I've had the following code, which
defines head function for using on list of existentials and coercing the head
back to original type according to type-level list:

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE TypeApplications #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE StandaloneKindSignatures #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE FlexibleContexts #-}
>
> import Data.Kind
> import Data.Proxy
> import Unsafe.Coerce
> import qualified GHC.Types as GHC.Types
>
> class FromTypeMaybe k where
>     type ToType k
>     fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
  
> instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
>     --type ToType 'Nothing = GHC.Types.Any
>     type ToType 'Nothing = t
>     fromTypeMaybe f _ x = Nothing
  
> instance forall (t :: Type). FromTypeMaybe ('Just @Type t) where
>     type ToType ('Just t) = t
>     fromTypeMaybe f _ x = Just (f x)
>
> type MaybeHead :: [t] -> Maybe t
> type family MaybeHead ts where
>     MaybeHead '[] = 'Nothing
>     MaybeHead (x ': xs) = 'Just x
>
> type Tail :: [t] -> [t]
> type family Tail ts where
>     Tail '[] = '[]
>     Tail (x ': xs) = xs
>
> data AnyData where
>     AnyData :: a -> AnyData
>
> unAny :: AnyData -> t
> unAny (AnyData x) = unsafeCoerce x
>
> headAny
>     :: forall ts
>     . FromTypeMaybe (MaybeHead ts)
>     => Proxy ts -> [AnyData] -> Maybe (ToType (MaybeHead ts))
> headAny _ [] = Nothing
> headAny _ (x : xs) = fromTypeMaybe unAny (Proxy @(MaybeHead ts)) x

This code works, when type-level list specified explicitly, like

     *Main> headAny @('[Int, Bool]) Proxy [AnyData 1, AnyData True]
     Just 1

but when i use 'Tail' function on type-level list with 1 element, it does not
work:

     *Main> headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True]

     <interactive>:22:1: error:
         • No instance for (Show *) arising from a use of ‘print’
         • In a stmt of an interactive GHCi command: print it

Though on list with many elements and with empty list everything works:

     *Main> headAny @(Tail '[]) Proxy [AnyData 1, AnyData True]
     Nothing

When i've tried to understand why, i've noticed some similarities between
working empty list case and non-working 1-element case: both these cases work
through 'Nothing instance of 'FromTypeMaybe' type class, but type variable t
is defined differently:

     *Main> :k! MaybeHead (Tail '[])
     MaybeHead (Tail '[]) :: Maybe t
     = 'Nothing
     *Main> :k! MaybeHead (Tail '[Bool])
     MaybeHead (Tail '[Bool]) :: Maybe *
     = 'Nothing

So, with empty list type variable t remains unbound, but with 1-element list
it is bound to Type. And then (ToType 'Nothing) is defined accordingly:

     *Main> :k! ToType (MaybeHead (Tail '[]))
     ToType (MaybeHead (Tail '[])) :: *
     = GHC.Types.Any
     *Main> :k! ToType (MaybeHead (Tail '[Bool]))
     ToType (MaybeHead (Tail '[Bool])) :: *
     = *

And, no surprise, that there's no (Show Type) instance:

     *Main> show $ headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True]

     <interactive>:38:1: error:
         • No instance for (Show *) arising from a use of ‘show’

Until that moment, i understand everything (i think).

But then ghc somehow manages to find Show instance for GHC.Types.Any (or may
be not, but how does it print result for empty list then?):

     *Main> show $ headAny @(Tail '[]) Proxy [AnyData 1, AnyData True]
     "Nothing"

And that's the first thing i don't understand: there's should be no Show instance,
but still..

Then i thought, that by defining (ToType 'Nothing) to be GHC.Types.Any instead
of t:

     instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
         type ToType 'Nothing = GHC.Types.Any
         fromTypeMaybe f _ x = Nothing

i may fix 1-element case. Type evaluation looked promising:

     *Main> :k! (MaybeHead (Tail '[]))
     (MaybeHead (Tail '[])) :: Maybe t
     = 'Nothing
     *Main> :k! ToType (MaybeHead (Tail '[]))
     ToType (MaybeHead (Tail '[])) :: *
     = GHC.Types.Any

but it does not work:

     *Main> show $ headAny @(Tail '[Bool]) Proxy [AnyData 1, AnyData True]

     <interactive>:44:1: error:
         • No instance for (Show GHC.Types.Any) arising from a use of ‘show’

     *Main> show $ headAny @(Tail '[]) Proxy [AnyData 1, AnyData True]

     <interactive>:45:1: error:
         • No instance for (Show GHC.Types.Any) arising from a use of ‘show’

And that's the second thing i don't understand: why it does not work, when i
explicitly define type to be equal to GHC.Types.Any?

Thanks.

PS. I've read "Any types" notes in GHC.Builtin.Types, but apart from that ghc
uses 'GHC.Types.Any' internally to unify (?) unconstrained types, i don't
understand much, sorry.


> 
> 
> 
>> On Jan 18, 2022, at 8:10 AM, Dmitriy Matrosov <sgf.dma at gmail.com> wrote:
>>
>>
>>
>> On 1/17/22 6:49 PM, Dmitriy Matrosov wrote:
>>>> {-# LANGUAGE DataKinds #-}
>>>> {-# LANGUAGE RankNTypes #-}
>>>> {-# LANGUAGE KindSignatures #-}
>>>> {-# LANGUAGE TypeApplications #-}
>>>> {-# LANGUAGE TypeOperators #-}
>>>> {-# LANGUAGE PolyKinds #-}
>>>> {-# LANGUAGE TypeFamilies #-}
>>>> {-# LANGUAGE GADTs #-}
>>>> {-# LANGUAGE StandaloneKindSignatures #-}
>>>> {-# LANGUAGE ScopedTypeVariables #-}
>>>> {-# LANGUAGE FlexibleContexts #-}
>>>>
>>>> import Data.Kind
>>>> import Data.Proxy
>>>> import Unsafe.Coerce
>>>> import qualified GHC.Types as GHC.Types
>>>>
>>>> class FromTypeMaybe k where
>>>>      type ToType k
>>>>      fromTypeMaybe :: (a -> ToType k) -> Proxy k -> a -> Maybe (ToType k)
>>>> instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
>>>>      --type ToType 'Nothing = GHC.Types.Any
>>>>      type ToType 'Nothing = t
>>>>      fromTypeMaybe f _ x = Nothing
>>>> instance forall (t :: Type). FromTypeMaybe ('Just @Type t) where
>>>>      type ToType ('Just t) = t
>>>>      fromTypeMaybe f _ x = Just (f x)
>>> then i've written a little more:
>>>> type MaybeHead :: [t] -> Maybe t
>>>> type family MaybeHead ts where
>>>>      MaybeHead '[] = 'Nothing
>>>>      MaybeHead (x ': xs) = 'Just x
>>>>
>>>> type Tail:: [t] -> [t]
>>>> type family Tail ts where
>>>>      Tail '[] = '[]
>>>>      Tail (x ': xs) = xs
>>>>
>>>> data AnyData where
>>>>      AnyData :: a -> AnyData
>>>>
>>>> unAny :: AnyData -> t
>>>> unAny (AnyData x) = unsafeCoerce x
>>>>
>>>> insertAny :: t -> [AnyData] -> [AnyData]
>>>> insertAny x zs = AnyData x : zs
>>>>
>>>> headAny
>>>>      :: forall ts
>>>>      . FromTypeMaybe (MaybeHead ts)
>>>>      => Proxy ts -> [AnyData] -> Maybe (ToType (MaybeHead ts))
>>>> headAny _ [] = Nothing
>>>> headAny _ (x : xs) = fromTypeMaybe unAny (Proxy @(MaybeHead ts)) x
>>> And now it works, when type-level list is explicitly specified, like:
>>>      *Main> headAny (Proxy @'[]) $  insertAny 1 $ insertAny True []
>>>      Nothing
>>>      *Main> headAny (Proxy @'[Int]) $  insertAny 1 $ insertAny True []
>>>      Just 1
>>>      *Main> headAny (Proxy @'[Int, Bool]) $  insertAny 1 $ insertAny True []
>>>      Just 1
>>> but if i use 'Tail' type-function first, it works only in two cases:
>>> for list with 2 or more elements
>>>      *Main> :t headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
>>>      headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
>>>        :: Maybe Int
>>>      *Main> headAny (Proxy @(Tail '[Bool, Int])) $  insertAny 1 $ insertAny True []
>>>      Just 1
>>> and empty list
>>>      *Main> :t headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
>>>      headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
>>>        :: Maybe t
>>>      *Main> headAny (Proxy @(Tail '[])) $  insertAny 1 $ insertAny True []
>>>      Nothing
>>> But for list with 1 element it does not work
>>>      *Main> :t headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
>>>      headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
>>>        :: Maybe *
>>>      *Main> headAny (Proxy @(Tail '[Bool])) $  insertAny 1 $ insertAny True []
>>>      <interactive>:246:1: error:
>>>          • No instance for (Show *) arising from a use of ‘print’
>>>          • In a stmt of an interactive GHCi command: print it
>>> .....
>>> And besides i don't see any way of fixing my (FromTypeMaybe 'Nothing)
>>> instance.
>>
>> I think, i've fixed everything. Eventually, it was very simple.
>>
>>> {-# LANGUAGE DataKinds #-}
>>> {-# LANGUAGE RankNTypes #-}
>>> {-# LANGUAGE KindSignatures #-}
>>> {-# LANGUAGE TypeApplications #-}
>>> {-# LANGUAGE TypeOperators #-}
>>> {-# LANGUAGE PolyKinds #-}
>>> {-# LANGUAGE TypeFamilies #-}
>>> {-# LANGUAGE GADTs #-}
>>> {-# LANGUAGE StandaloneKindSignatures #-}
>>> {-# LANGUAGE ScopedTypeVariables #-}
>>> {-# LANGUAGE FlexibleInstances #-}
>>> {-# LANGUAGE MultiParamTypeClasses #-}
>>>
>>> import Data.Kind
>>> import Data.Proxy
>>> import Unsafe.Coerce
>>>
>>> class FromTypeMaybe2 k t where
>>>     fromTypeMaybe2 :: (a -> t) -> Proxy k -> a -> Maybe t
>>>
>>> instance FromTypeMaybe2 'Nothing t where
>>>     fromTypeMaybe2 f _ _ = Nothing
>>>
>>> instance (t ~ t') => FromTypeMaybe2 ('Just t) t' where
>>>     fromTypeMaybe2 f _ x = Just (f x)
>>>
>>> headAny2
>>>     :: forall t ts
>>>     . FromTypeMaybe2 (MaybeHead ts) t
>>>     => Proxy ts -> [AnyData] -> Maybe t
>>> headAny2 _ [] = Nothing
>>> headAny2 _ (x : xs) = fromTypeMaybe2 unAny (Proxy @(MaybeHead ts)) x
>>>
>>> type MaybeHead :: [t] -> Maybe t
>>> type family MaybeHead ts where
>>>     MaybeHead '[] = 'Nothing
>>>     MaybeHead (x ': xs) = 'Just x
>>>
>>> type Tail:: [t] -> [t]
>>> type family Tail ts where
>>>     Tail '[] = '[]
>>>     Tail (x ': xs) = xs
>>>
>>> data AnyData where
>>>     AnyData :: a -> AnyData
>>>
>>> unAny :: AnyData -> t
>>> unAny (AnyData x) = unsafeCoerce x
>>
>> And now everything works:
>>
>>     *Main> headAny2 (Proxy @'[]) $ [AnyData 1, AnyData True]
>>     Nothing
>>     *Main> headAny2 (Proxy @'[Int]) $ [AnyData 1, AnyData True]
>>     Just 1
>>     *Main> headAny2 (Proxy @'[Int, Bool]) $ [AnyData 1, AnyData True]
>>     Just 1
>>
>> and
>>
>>     *Main> headAny2 (Proxy @(Tail '[Bool, Int])) $ [AnyData 1, AnyData True]
>>     Just 1
>>     *Main> headAny2 (Proxy @(Tail '[Bool])) $ [AnyData 1, AnyData True]
>>     Nothing
>>     *Main> headAny2 (Proxy @(Tail '[])) $ [AnyData 1, AnyData True]
>>     Nothing
>>
>> The only question, that remains is why defining 'Nothing resulting type to be
>> 'GHC.Types.Any' in previous implementation
>>
>>     instance forall (t :: Type). FromTypeMaybe ('Nothing @t) where
>>         type ToType 'Nothing = GHC.Types.Any
>>
>> does not fix it?
>> _______________________________________________
>> 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.
>