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
Conversation
Replying to
Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!
2
Replying to
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)
1
1
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! 😅
2
Heh, I think you might be onto something there - would have to figure out if there’s a way to draw that 🤔
1
2
Show replies
Replying to
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...
1
1
Oh sweeet - was hoping I was somehow recreating something badly…