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 🤔

Replying to

and

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…

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

Replying to

and

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

Jules Jacobs

@JulesJacobs5

Apr 29, 2021

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.

Show replies