Conversation

Rob Rix‎
@rob_rix
a telescope is a way of looking at function types. { A : Type } -> A -> Int can be flattened down into e.g. ([{ A : Type }, ( _ : A) ], Int). the list is basically a context, and each name in it can be used in the types of later entries, as well as in the body.
1
3
Rob Rix‎
@rob_rix
a neutral spine is a representation for values used in normalization-by-evaluation consisting of a variable at the head, followed by a (snoc) list of eliminations (e.g. values to apply the value the variable represents to). f a 0 can be flattened down into (f, Nil :> a :> 0)
1
2
Rob Rix‎
@rob_rix
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.
1
3
Rob Rix‎
@rob_rix
if f’s type is described as a telescope, then the types of its eliminations (arguments) will be the types in the telescope’s context, and the neutral term as a whole will have the final result type of the telescope.
2
4
Jacques Carette
@jjcarett2
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
Jacques Carette
@jjcarett2
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
Brendan Zabarauskas
@brendanzab
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
Rob Rix‎
@rob_rix
I’m struggling to even make things work at the moment; inefficiency would be a nice problem to have, from that perspective ^_^;;
1
2
Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
@rob_rix
and
@jjcarett2
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
Show replies