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
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
Show replies