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

[Richard Eisenberg]

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?

Thanks,
Richard



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