Conversation

I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these ✨very informal✨ Venn diagram thingies: gist.github.com/brendanzab/68f

BNF gammar and Venn diagram of the syntax of a dependently typed language

read image description

ALT

BNF gammar and Venn diagram of the semantic domain of a dependently typed language

read image description

ALT

Jules Jacobs

@JulesJacobs5

Apr 29, 2021

Nice. Why can't types be neutral terms?

Brendan Zabarauskas

@brendanzab

Apr 29, 2021

Heh, I think you might be onto something there - would have to figure out if there’s a way to draw that 🤔

Brendan Zabarauskas

@brendanzab

Apr 29, 2021

Been playing around - I guess it might be a bad idea to have 'Type' and 'Expression' on here because you can only really know that with contextual information? Like a variable or an eliminator could be types, depending on what is in the environment…

Replying to

and

Perhaps it could be possible to represent the possible worlds(?) somehow, in a graphical way? 🤔

12:53 PM · Apr 29, 2021Twitter Web App

Replying to

Yeah I think the classification of terms as neutral or not is orthogonal to whether it's a type or not. A term is not neutral (reactive?) if it beta normalises to an introduction form. Otherwise it is neutral.

Jules Jacobs

@JulesJacobs5

Apr 29, 2021

For types I think we can say that we have typed terms (where each binder is annotated with a type), and from these terms we can compute a new term that is its type.

Show replies