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

Replying to

@JulesJacobs5

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

9:39 AM · Apr 29, 2021Twitter for iPhone

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…

Brendan Zabarauskas

@brendanzab

Apr 29, 2021

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

Show replies