[Haskell-cafe] Coercing existential according to type-level Maybe (re-post from h-beginners)
Dmitriy Matrosov
sgf.dma at gmail.com
Thu Jan 27 15:25:52 UTC 2022
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.
>
More information about the Haskell-Cafe
mailing list