Using GADT constructor kinds in its return type - Haskell

I'm using DataKinds to promote the GADT constructors as types, such that I can restrict the FooList return type to contain just a list of Foo. In Foo this type is duplicated, but in Bar we use constructor kind to respect DRY.

data Foo a where
  FooOne :: Text -> Foo Int
  FooList :: Foo [(Text, Int)]

type C (c :: Bar a) = (Bar a, a)

data Bar a where
  BarOne :: Text -> Bar Int
  BarList :: Bar [C ('BarOne arg)]

However GHC does not compile Bar as it throws:

error:
    • Type constructor ‘Bar’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the kind ‘Bar a’
   |
30 | type C (c :: Bar a) = (Bar a, a)
   |              ^^^

Is there a different way to achieve this?

(Imagine Foo having many such pairs of constructors (one for singleton, and another for list of it), and our goal here is to have the list constructors to use the same type as the singletone constructor in its return type, without duplicating the types by hand (which makes it error-prone, and more complex to read)

@Sridhar Ratnakumar Sometimes you can "tie the knot" in type (as we do with Sem's row in polysemy), but personally I don't see how to make this work
Maybe try splitting that list thing into separate GADT and parametrize by types involved?

Or maybe you want something completely different? What's the use case?

@TheMatten The use case is to represent the different "routes" in my static web site, such that each route specifies (in the type parameter of GADT) the type of the data used to generate the final HTML. Here's the real definition: https://github.com/srid/website/blob/0d36d459b5f226192d5138ab75a2f8d8aed6735d/src/Website/Page.hs#L30-L39

So Route_Note represents an individual note page, whereas Route_Index represents the main page which links to all the note pages, and thus its value type includes a list of routes to those notes (along with the 'value' of each route)

The main reason for pushing the date value type to GADT type parameter is so that I can write functions like urlForRoute :: Route a -> Text without requiring that data to be present. If I'm passing a list of routes to a breadcrumb function, for example, I just won't have the value for all routes obviously.

(Where I do need the value, such as in a function that renders the HTML, I would use DSum Route Identity)

I would maybe consider something like:

data Route = Index | Note | Tidbit

data SRoute :: Route -> Type where
  SIndex  :: SRoute 'Index
  SNote   :: SRoute 'Note
  STidbit :: SRoute 'Tidbit

type family RouteData :: Route -> Type where
  RouteData 'Index  = (MMark, [(SourcePath, MMark)])
  RouteData 'Note   = MMark
  RouteData 'Tidbit = [(SourcePath, Tidbit)]

type family RouteOutput :: Route -> Type where
  RouteOutput 'Index  = 'HTML
  RouteOutput 'Note   = 'HTML
  RouteOutput 'Tidbit = 'HTML

getPageMeta :: SRoute r -> RouteData r -> Maybe SrcMeta

Interesting; type families is something I've never considered ...

(One thing I'd eventually like to support is recursive routes, so: data Route = Index | Note | Tidbit TidbitRoute)

@TheMatten How would you define a function that renders only HTML routes (renderHtml :: DSum (Route 'HTML) Identity -> Html ()) for these type-family based types?

Real code: https://github.com/srid/website/blob/0d36d459b5f226192d5138ab75a2f8d8aed6735d/src/Main.hs#L103-L104

renderHtml :: RouteOutput r ~ 'HTML => SRoute r -> RouteData r -> Html ()

Constraining without type classes. Hmm.

By having simple singleton and branching in type level functions I avoid coupling potentially unrelated information in one GADT - in a way, your original datatype was sort of "double function", computing two different things at the same time. That doesn't scale when you decide track some new property of route - you would have to unnecessarily update and clutter bunch of unrelated code.

I try to think in "dependent" way - If Haskell was a dependent language, how would I write such code? I would take normal ADTs and compute types based on them.
And then in real Haskell, I simply swap dependent quantifiers for singletons.

As an aside: I'm quite happy to have stumbled upon type famillies through an actual use case need ... because this makes 'connecting the dots' easier, and learning intermediate/ advanced Haskell more practical (rather than as a detached academic knowledge)

Once you start working with values at type level, they're somewhat inevitable :big_smile: (Ignoring MultiParamTypeClasses with FunctionalDependencies, which were used for same purposes historically)

This is rad. Case on the singleton, and then unpack the actual route data. Can you do this without anonymous functions though?

renderHtml :: RouteOutput r ~ 'HTML => SRoute r -> RouteData r -> Html ()
renderHtml = \case
  SIndex -> \(_doc, _notes) -> undefined
  SNote -> \_doc -> undefined
  STidbit -> \_tidbits -> undefined

So, to resolve the original problem I replaced RouteData 'Index = (MMark, [(SourcePath, MMark)]) with RouteData 'Index = (MMark, [(Route 'Note, RouteData 'Note)]) (and then enabled UndecidableInstances).

I think the next step is to group this singleton type and the type families in a type class IsRoute, so that recursive route kinds can simply implement an instance of it. And throw in utility functions like routeFile or routeUrl in it.

Not sure if I see how that would work

Trying to make it work. Seems I need either IsRoute and/or a kind of kind? (kind of all route kinds)

IsRoute makes sense for cases where route is statically determined - is that case in methods you want it to have?

All routes are static. It is just that I'll have sub routes in separate modules, with the "top level" route pulling them all in.

Real code example: added a TidbitRoute sub route (and the associated type familly declarations): https://github.com/srid/website/blob/e0e4b3de3e5c4db8d61ec4d2475e61016be7ea17/src/Website/Route.hs#L26-L29

Wait, so you know what route you're passing to e.g. renderHtml?

(see the modified renderHtml in that link)

I wouldn't know what route I'm passing to it, no. It can be any r, as long as RouteOutput r ~ 'HTML.

Because then you don't want singletons at all - they can all be methods of IsRoute

I assume singleton type is being defined here only because non-Type kinds cannot be inhabited in Haskell.

Also notice how in that link a new type family (eg: TidbitRouteData) gets defined for each sub route. This is one reason behind the type class approach, as I thought that putting the type family inside the type class would obviate new definitions.

Singletons are used to lift values to type level - there's no way of saying "this value determines that type" - so they "cheat" by having only one value for every different final type

But if they're available at compile time, you can just as well put them directly into types and not use singletons at all

How would the above renderHtml look like without singletons?

Note that each route has its own "datum" and "output" type.

This would typecheck:

data Foo = Bar | Baz

data SFoo :: Foo -> Type where
  SBar :: SFoo 'Bar
  SBaz :: SFoo 'Baz

class IsFoo (foo :: Foo) where
  withBar :: foo ~ 'Bar => ()

instance IsFoo 'Bar where
  withBar = ()

instance IsFoo 'Baz where
  withBar = case refl @_ @'Baz @'Bar of {}

refl :: forall k (a :: k) (b :: k). a ~ b => a :~: b
refl = Refl

But I guess it wouldn't be that convenient to write - thing is, keeping value at type level for as long as possible makes working with them easier

My attempt at writing a IsRoute mostly succeeded, except when it came to implementing the type family. Apparently you cannot write multiple instances for it (one for each kind constructor) inside a type class instance, as the compile disallows it. Anyway, it seemed to me that type-class'fying it would complicate things a bit for little benefit.

@TheMatten I've incorporated your suggestions in here: https://github.com/srid/website/pull/15/files ... the new route system is a little more complex than I'd like, but things are much easier to modify from now. Thanks for the help! Good to learn about type families ...