[Haskell-cafe] restore type from existential

[Georgi Lyubenov]

Another thing which I forgot to mention - if you absolutely need to have 
an existential, i.e. `MyTypes` should not be visible at the top level,
you'll need to also include some existential wrapper for the versions of 
`Wrap` together with a singleton for the type level list,
in order to be able to later at runtime recover what the original list 
of types was.

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.