Conversation

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

(in that you can apply them explicitly, not in that you have to. this isn’t done yet either tho)

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Brendan Zabarauskas

@brendanzab

Bounded polymorphism and typeclasses - ideas · Issue #502 · unisonweb/unison

I think I remember the Unison folks thinking about doing something similar with their 'abilities'?

github.com

I wanted to throw in my tuppence on what Unison could do about typeclasses (see comment below) so I'm opening this issue as a place to put such things. I'm aware that this is one of...

Replying to

and

Dunno where in this conversation this is relevant, but there was also this interesting blog post: blog.ezyang.com/2020/08/dynami Following the Granule stuff with interest - coeffects seem really cool!

8:20 PM · Oct 26, 2020Twitter Web App

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Brendan Zabarauskas

@brendanzab