Conversation

Rob Rix‎
@rob_rix
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
1
2
Rob Rix‎
@rob_rix
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)
1
Rob Rix‎
@rob_rix
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
1
1
Rob Rix‎
@rob_rix
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
1
Rob Rix‎
@rob_rix
(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
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more