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.