[Haskell-cafe] restore type from existential

[Georgi Lyubenov]

Hi Zoran,

If you've decided to use an "index" type family like `TypeOf`, you don't 
need unsafeCoerce:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

type MyTypes = '[(), Char, Int]

data N = Z | S N

type family TypeOf n lst where
   TypeOf 'Z (t ': ts) = t
   TypeOf ('S n) (t ': ts) = TypeOf n ts

data SNat (n :: N) where
   SZ :: SNat 'Z
   SS :: SNat n -> SNat ('S n)

data Wrap where
   MkWrap :: SNat n -> TypeOf n MyTypes -> Wrap

t1, t2, t3 :: Wrap
t1 = MkWrap SZ ()
t2 = MkWrap (SS SZ) 'x'
t3 = MkWrap (SS (SS SZ)) 1

unwrap :: Wrap -> (forall n. (Show (TypeOf n MyTypes)) => TypeOf n 
MyTypes -> res) -> res
unwrap (MkWrap ix val) f =
   case ix of
     SZ -> f @Z val
     SS SZ -> f @(S Z) val
     SS (SS SZ) -> f @(S (S Z)) val

main :: IO ()
main = do
   unwrap t1 print
   unwrap t2 print
   unwrap t3 print


The "unsafe" approach I was referring to was much more involved than I 
recall, you can check Chapter 11. Extensible Data
from the "Thinking with Types" (Sandy Maguire) book for more information.

In general, it seems to me that what you're looking for is roughly the 
same thing as extensible sums/records, so it might
also be beneficial for you to look into some libraries that provide 
those, and how they've achieved `Wrap`?

Cheers,
Georgi


On 1/10/24 15:40, zoran.bosnjak at via.si wrote:
> Hi Georgi,
> thanks for your response. I am not sure I fully understand your 
> suggestion with 'unsafe' approach. In particular:
>
> It is not clear to me how could I drop SNat and use Int instead. How 
> do I suppose to get type information out of plain Int?
> Could you please show an example of the actual 'unwrap' function?
>
> This is my current attempt. The problem is that I need to provide type 
> annotation to the unwrap result, which I would like to avoid if possible.
>
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeFamilies #-}
>
> import Unsafe.Coerce
>
> type MyTypes = '[(), Char, Int]
>
> data N = Z | S N
>
> type family TypeOf n lst where
>     TypeOf 'Z (t ': ts) = t
>     TypeOf ('S n) (t ': ts) = TypeOf n ts
>
> data SNat (n :: N) where
>     SZ :: SNat 'Z
>     SS :: SNat n -> SNat ('S n)
>
> data Wrap where
>     MkWrap :: TypeOf n MyTypes ~ t => SNat n -> t -> Wrap
>     -- MkWrap :: SNat n -> TypeOf n MyTypes -> Wrap
>
> t1, t2, t3 :: Wrap
> t1 = MkWrap SZ ()
> t2 = MkWrap (SS SZ) 'x'
> t3 = MkWrap (SS (SS SZ)) 1
>
> unwrap :: Wrap -> t
> --unwrap (MkWrap (ix :: SNat n) (val :: t)) = unsafeCoerce val
> unwrap (MkWrap _ix val) = unsafeCoerce val
>
> main :: IO ()
> main = do
>     print $ (unwrap t1 :: ())
>     print $ (unwrap t2 :: Char)
>     print $ (unwrap t3 :: Int)
>
> Zoran
>
> On 2024-01-10 12:57, Georgi Lyubenov wrote:
>> Hi Zoran,
>>
>> No, with your given Wrap data type, it would not be possible.
>>
>> The moment you only constraint `t` to be `forall` bound in 
>> `WrapUnsafe` and have not other properties, there's really no way to 
>> get it out without using `unsafeCoerce`.
>>
>> There are many approaches to achieve being able to "recover" what `t` 
>> is.
>>
>> One idea would be to add a list type parameter `ts` to `Wrap` and a 
>> constraint to `WrapUnsafe` which says "t is the type at index n in 
>> the list ts", i.e. something like
>> ```
>> type family Index n ts where
>>   Index 0 (t ': _) = t
>>   -- might need your own definition of Nat for the next case
>>   Index (1 + n) (_ ': ts) = Index n ts
>>
>> data Wrap ts where
>>   MkWrap :: SNat n -> Index n ts -> Wrap ts
>> ```
>>
>> Another (which I personally think is cleaner) would be to entirely 
>> skip the `SNat`s and use an "membership proof" instead, i.e. 
>> something like
>> ```
>> data Elem (x :: t) (xs :: [t]) where
>>   Here :: Elem x (x ': xs)
>>   There :: Elem x xs -> Elem x (y ': xs)
>> ```
>> You could then have
>> ```
>> data Wrap ts where
>>   MkWrap :: Elem t ts -> t -> Wrap ts
>> t1, t2, t3 :: Wrap MyTypes
>> t1 = MkWrap Here ()
>> t2 = MkWrap (There Here) 'x'
>> t3 = MkWrap (There (There Here)) 1
>> ```
>> You could then also try to automate the membership proof generation 
>> via type classes.
>>
>> If you're going the unsafe approach and going to be 
>> `unsafeCoerce`ing, you could also just as well drop the `SNat` and 
>> use a raw `Int` instead,
>> because you're the one who's going to be taking care not to 
>> `unsafeCoerce` the wrong thing anyways.
>>
>> Cheers,
>> Georgi
>>
>> On 1/10/24 12:25, zoran.bosnjak at via.si wrote:
>>> Dear haskellers,
>>> if for example I have the following (simplified) situation:
>>>
>>> import GHC.TypeLits
>>>
>>> type MyTypes =
>>>     '[ ()    -- index 0
>>>      , Char  -- index 1
>>>      , Int   -- index 2
>>>      ]
>>>
>>> data SNat (n :: Nat) where
>>>     SZ :: SNat 0
>>>     SS :: SNat n -> SNat (n+1)
>>>
>>> data Wrap where
>>>     WrapUnsafe :: SNat n -> t -> Wrap
>>>
>>> t1 = WrapUnsafe SZ () :: Wrap
>>> t2 = WrapUnsafe (SS SZ) 'x' :: Wrap
>>> t3 = WrapUnsafe (SS (SS SZ)) (1::Int) :: Wrap
>>>
>>> Is it possible to have an 'unwrap' function? That is: to combine 
>>> MyType types table and the type index... to get the exact type back. 
>>> Something in the form:
>>>
>>> unwrapUnsafe :: Wrap -> t
>>> unwrapUnsafe (WrapUnsafe (ix::SNat n) (val::t)) = undefined
>>>
>>> x1 = unwrapUnsafe t1
>>> x2 = unwrapUnsafe t2
>>> x3 = unwrapUnsafe t3
>>>
>>> GHC didn't like any of my attempt. Is it even possible?
>>>
>>> regards,
>>> Zoran
>>> _______________________________________________
>>> 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.
>> _______________________________________________
>> 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.