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

26 Jan 2022

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

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

Richard Eisenberg