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

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