<p dir="ltr">The `singletons`[1] library is as convienient as you can get in Haskell.</p>
<p dir="ltr">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.</p>
<p dir="ltr">[1]: <a href="https://hackage.haskell.org/package/singletons">https://hackage.haskell.org/package/singletons</a></p>
<br><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">On Thu, 19 Dec 2024, 19:39 Zoran Bošnjak, <<a href="mailto:zoran.bosnjak@via.si">zoran.bosnjak@via.si</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear haskell cafe,<br>
I would like to describe some structures as types (something like <br>
servant does) and I would also need to use the same structure in <br>
run-time as a value. I am trying to figure out how could I use <br>
GHC.Generics or something to do this for several user defined <br>
structures.<br>
<br>
Currently I am doing it manually (with does not work, but it might serve <br>
as intention), for example:<br>
<br>
-- generic example structure<br>
data GTest s n = GTest0 | GTest1 s | GTest2 n<br>
<br>
type TTest = GTest Symbol Nat     -- type level<br>
type VTest = GTest String Integer -- value level<br>
<br>
For all my user defined structure, at the type level it will always be <br>
only (Symbol, Nat) which should translate to (Text, Int) or (String, <br>
Integer) for simplicity.<br>
<br>
-- | Convert schema from type to value<br>
class IsSchema t a where<br>
     schema :: a<br>
<br>
instance KnownNat n => IsSchema n Integer where<br>
     schema = natVal (Proxy @n)<br>
<br>
instance KnownSymbol s => IsSchema s String where<br>
     schema = symbolVal (Proxy @s)<br>
<br>
instance IsSchema 'GTest0 VTest where<br>
     schema = GTest0<br>
<br>
instance<br>
     ( IsSchema s String<br>
     ) => IsSchema ('GTest1 s) VTest where<br>
     schema = GTest1 (schema @s)<br>
<br>
instance<br>
     ( IsSchema n Integer<br>
     ) => IsSchema ('GTest2 n) VTest where<br>
     schema = GTest2 (schema @n)<br>
<br>
I would like to generalize the process, by saying something like (not <br>
sure if I even need this):<br>
<br>
data Usage = TypeLevel | ValueLevel<br>
<br>
data GTest ? = Gtest0 | GTest1 ? | GTest2 ? (deriving ?)<br>
<br>
... and be able to use the same Test structure in both cases, such as:<br>
<br>
Use it as a phantom type in some other type:<br>
<br>
data Item (t :: TTest) where<br>
     Item0 :: Item 'GTest0<br>
     Item1 :: String -> Item ('GTest1 s)<br>
     Item2 :: Integer -> Item ('GTest2 n)<br>
<br>
And use it as value, something like:<br>
<br>
data SomeItem = forall t a. IsSchema t a => SomeItem a (Item t)<br>
<br>
In other words... I would like to work with exact types (Item t) or <br>
generically with SomeItem, when the type is not exactly known, but the <br>
value level schema is known.<br>
<br>
I came far with manual approach, but I could not create SomeItem from <br>
the value schema. So, for example this does not compile (the error is <br>
about KnownSymbol/KnownNat):<br>
<br>
mkSomeItem :: VTest -> SomeItem<br>
mkSomeItem sch = case sch of<br>
     GTest0 -> SomeItem sch Item0<br>
     GTest1 s -> SomeItem sch (Item1 (s <> s))<br>
     GTest2 n -> SomeItem sch (Item2 (succ n))<br>
<br>
I am curious to know how to fix this problem. But the manual conversion <br>
approach is something I would like to avoid in the first place. <br>
Appreciate your help.<br>
<br>
regards,<br>
Zoran<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>