[Haskell-cafe] convert structures from type to value level

[Isaac Elliott]

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, <zoran.bosnjak at via.si> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20241220/bd53e104/attachment.html>