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