[Haskell-cafe] restore type from existential

[Georgi Lyubenov]

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.