Conversation

I’m struggling to even make things work at the moment; inefficiency would be a nice problem to have, from that perspective ^_^;;

Yeah, well... I guess I have ideas how to make it work but that might not work in reality ; _ ; just hate how positional all the currying and pairing stuff is - as much as it's nice in some cases then stuff lines up properly

I had this weird (probably bad) idea to have records with 'abstract' fields that you could make concrete later - which would end up kind of being like functions? And you'd be able to have a 'default' field that your record would reduce to if all the fields were concrete.

Rob Rix‎

@rob_rix

not sure I totally get this; how would it contrast with having a field with function type?

PhD research ;; What’s the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

Records with abstract fields are kind of like functions. But there would be sugar on top to make it look more familiar. Hoping this might help with the issues around bundled and unbundled modules: alhassy.github.io/next-700-modul - but I dunno.

alhassy.github.io

next-700-module-systems

So you'd have: { ?A : Type, op : [A, A] -> A, } Which could be sugar for: { ?A : Type, op : { ?0 : A, ?1 : A, default : A }, }

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], }

1:30 AM · Oct 26, 2020Twitter Web App

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

Replying to

and

But this might break a bunch of nice stuff in the type system and might be a really ✨Bad✨ idea. 😅

Replying to

and

Like I think generally it's considered good to have nice categorical models of your type systems, and alterations like this might break a bunch of that stuff? Or at least be a rather ad-hoc extension? All the category theory stuff is a bit mysterious to me though. 😰

Rob Rix‎

@rob_rix

yeah, I can usually make *some* headway on a sequent calculus judgement, but once the category theory’s out I might as well just drink

Show replies

Replying to

and

All my instincts tell me that this particular variant is indeed a Bad Idea. You want your 'functions' to be continuous - which, in this case, means given by a uniform definition of the inputs. But in the same neighborhood of this idea, I'm sure there are some good designs.