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.
Conversation
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.
1
1
So you'd have:
{
?A : Type,
op : [A, A] -> A,
}
Which could be sugar for:
{
?A : Type,
op : { ?0 : A, ?1 : A, default : A },
}
1
1
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],
}
2
1
This:
add-int-magma.op.[1, 3]
would elaborate to:
add-int-magma.op.{0 = 1, 1 = 3}.default
2
1
But this might break a bunch of nice stuff in the type system and might be a really ✨Bad✨ idea. 😅
2
2
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. 😰
1
Replying to
Heh, don't know much about the sequent calculus - have only really messed around with natural deduction. Takes a long time to get my head around the judgements though - especially if they aren't presented in a syntax-directed style.
Yeah me too - I think sequent calculus can have multiple conclusions to the right of the turnstile? But I think there are deeper things than that - I've just never seen a side-by-side comparison. I think for whatever reason in PL research natural deduction is more popular?
2
Show replies