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
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.
2
2
Thanks! I will ponder more - definitely feel like I'm missing something. I was thinking of today was that:
Σ (a : A). Π (b : B). C a b
can be reordered to:
Π (b : B). Σ (a : A). C a b
but converse is not true, unless I'm horribly mistaken. 🤔
1
So yeah, this seems of runs against what I'd want for entries being re-orderable, and hints at some finer details I might be missing.
You can re-order non-dependent nested Π or Σ, but the other re-ordering depends on your meta-theory since it's equivalent to a version of the axiom of choice! In the first case, that's just saying the products and sums are up-to-iso commutative.
1