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

Sasha

@Sasha_Boyd

Apr 30, 2021

Watch out, first you start drawing Venn diagrams of type systems, and it seems innocent enough, but eventually you find yourself stuck in the middle of the ocean, babbling about topos theory. I've seen it happen to too many good people...

Brendan Zabarauskas

@brendanzab

Replying to

@Sasha_Boyd

Oh sweeet - was hoping I was somehow recreating something badly…

12:03 AM · Apr 30, 2021Twitter Web App