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

Nnotm

@nnotm

Apr 29, 2021

Hm, does being "stuck" mean being in some sort of normal form? If so, it seems like both elim without intro and intro without elim would produce a stuck term (but diagram only shows elim in the stuck category)

Brendan Zabarauskas

@brendanzab

Replying to

@nnotm

Stuck things are values that can’t reduce further because the ‘head’ is something like a variable. You usually hear them called ‘neutral values’ but I couldn’t find any explanation for that name. Maybe it’s more confusing than less though, sorry! 😅

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

Likes