telescopes are type-y things, spines are term-y things (tho note you can have kind-level telescopes and type-level spines), and they grow at opposite ends; but a telescope can describe the type of a neutral spine.
Conversation
You should also notice that telescopes, contexts (in a DTT), theory presentations, specifications, module signatures, records-as-Sigma-types and traits are also essentially all the same, especially in a dependently typed setting.
2
12
In general, we have uses for a generic idea of defining some valid X (which can be a type or a term or ...) using names in scopes as part of the definition of X. These naturally for a DAG (unless you go for mutual recursion too).
2
2
I do wish that telescopes and spines were less... listy... and more... graphy. So that more telescopes were equivalent, and more spines could be checked against them. That's why I find records and labelled args nice. Just unsure how to make it efficient in an implementation. 😰
1
3
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
1
1
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.
2
1
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
[Replying to this whole thread]. Like how you refer to my PhD student's work for the unbundling problem 😆. And yes, contexts should be at least DAGs, not lists. (mutual can involve local cycles too...). Records with abstract fields are quite common in math. 1/
1
2
Show replies
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
Show replies