You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
is a "superclass" of a corresponding constructor class:
classForall (WhatCf) =>DfwheremapIt:: (a->b) ->fa->fbinsert1::Df=>a->fa->fa
insert1 =-- something using `inst`
Unfortunately, each such case must currently be constructed entirely by hand. Is there some way we can do this "generically", letting the user provide some representation of the structure of a constraint expression, where the holes should be, and (ugh) which holes should be tied together?
The text was updated successfully, but these errors were encountered:
I build up a bunch of interesting constructions in the category of constraints in my ekmett/hask package, maybe some of those ideas will help you. I'm not sure how well the result would fit here in the scope of this package though.
I had an idea purely in my mind last autumn of doing something like this with de Bruijn indices and a Constraint-returning continuation monad in the type system.
Then I realized this was not just crazy, but also ridiculously verbose, and thought up InstV instead.
The current tools can do a lot of things. For instance:
Forall
can also do other fancy things:Now
Forall (What con s)
means that for allc
, the constraintcon c (s c)
holds. This can be used to express that a class likeis a "superclass" of a corresponding constructor class:
Unfortunately, each such case must currently be constructed entirely by hand. Is there some way we can do this "generically", letting the user provide some representation of the structure of a constraint expression, where the holes should be, and (ugh) which holes should be tied together?
The text was updated successfully, but these errors were encountered: