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