The `singletons`[1] library is as convienient as you can get in Haskell. I find the second half of your question is confusing, but it seems like you're asking, "how do I make Haskell *truly* dependently typed". The answer being: you can't, so you use `singletons` while accepting the pain, or change to a dependently typed language like Agda or Idris. [1]: https://hackage.haskell.org/package/singletons On Thu, 19 Dec 2024, 19:39 Zoran Bošnjak, wrote:

Dear haskell cafe, I would like to describe some structures as types (something like servant does) and I would also need to use the same structure in run-time as a value. I am trying to figure out how could I use GHC.Generics or something to do this for several user defined structures.

Currently I am doing it manually (with does not work, but it might serve as intention), for example:

-- generic example structure data GTest s n = GTest0 | GTest1 s | GTest2 n

type TTest = GTest Symbol Nat -- type level type VTest = GTest String Integer -- value level

For all my user defined structure, at the type level it will always be only (Symbol, Nat) which should translate to (Text, Int) or (String, Integer) for simplicity.

-- | Convert schema from type to value class IsSchema t a where schema :: a

instance KnownNat n => IsSchema n Integer where schema = natVal (Proxy @n)

instance KnownSymbol s => IsSchema s String where schema = symbolVal (Proxy @s)

instance IsSchema 'GTest0 VTest where schema = GTest0

instance ( IsSchema s String ) => IsSchema ('GTest1 s) VTest where schema = GTest1 (schema @s)

instance ( IsSchema n Integer ) => IsSchema ('GTest2 n) VTest where schema = GTest2 (schema @n)

I would like to generalize the process, by saying something like (not sure if I even need this):

data Usage = TypeLevel | ValueLevel

data GTest ? = Gtest0 | GTest1 ? | GTest2 ? (deriving ?)

... and be able to use the same Test structure in both cases, such as:

Use it as a phantom type in some other type:

data Item (t :: TTest) where Item0 :: Item 'GTest0 Item1 :: String -> Item ('GTest1 s) Item2 :: Integer -> Item ('GTest2 n)

And use it as value, something like:

data SomeItem = forall t a. IsSchema t a => SomeItem a (Item t)

In other words... I would like to work with exact types (Item t) or generically with SomeItem, when the type is not exactly known, but the value level schema is known.

I came far with manual approach, but I could not create SomeItem from the value schema. So, for example this does not compile (the error is about KnownSymbol/KnownNat):

mkSomeItem :: VTest -> SomeItem mkSomeItem sch = case sch of GTest0 -> SomeItem sch Item0 GTest1 s -> SomeItem sch (Item1 (s <> s)) GTest2 n -> SomeItem sch (Item2 (succ n))

I am curious to know how to fix this problem. But the manual conversion approach is something I would like to avoid in the first place. Appreciate your help.

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.