[Haskell-cafe] restore type from existential

[zoran.bosnjak at via.si]

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.