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.
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)
| ^^^
(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?
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.
@TheMatten How would you define a function that renders only HTML routes (renderHtml :: DSum (Route 'HTML) Identity -> Html ()) for these type-family based types?
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)
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.
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
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 ...
I'm using
DataKinds
to promote the GADT constructors as types, such that I can restrict theFooList
return type to contain just a list ofFoo
. In Foo this type is duplicated, but in Bar we use constructor kind to respect DRY.However GHC does not compile
Bar
as it throws: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 inpolysemy
), but personally I don't see how to make this workMaybe 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, whereasRoute_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 abreadcrumb
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:
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
withFunctionalDependencies
, 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?So, to resolve the original problem I replaced
RouteData 'Index = (MMark, [(SourcePath, MMark)])
withRouteData '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 likerouteFile
orrouteUrl
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-L29Wait, 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 asRouteOutput 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:
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 ...