Conversation

And then something like this maybe: { add-int-magma : Magma.{A = Int} = { op = [x, y] => x + y, }, test-add-int : Int = add-int-magma.op.[1, 3], }

Brendan Zabarauskas

@brendanzab

This: add-int-magma.op.[1, 3] would elaborate to: add-int-magma.op.{0 = 1, 1 = 3}.default

it finally clicked that the same situation arises in Facet, and that I have a broadly similar approach to solving it (not yet implemented) basically, Facet approaches inversion of control/ad hoc polymorphism via effects. no typeclasses or module signatures, just effects

so for example a Monoid is also a Semigroup: interface Semigroup : (S : Type) -> Interface { _ <> _ : S -> S -> [Semigroup S] S } interface Monoid : (S : Type) -> [Semigroup S] Interface { unit : [Monoid S] S } (brackets mean “needs this effect” so a Monoid needs a Semigroup)

in a sense, Monoid implies Semigroup, but for richer structures the implication might mean “implements” and you should be able to obtain a default definition for the simpler structure given only the richer one, and I intend to do that by allowing effects to offer defaults

extending that further I plan on allowing defaults to specified for a given scope (definition, module, file, project) so you can say e.g. that lists are usually a monoid by appending with the empty list. but if you really really want the elementwise monoid you can use it locally

(I’m also planning on tackling records using effects but I haven’t thought it out fully yet.) this is a simpler space, since it’s not currently dependently typed, but it is at least Fω + effects; explicit type applications and all