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.