“Dynamically typed languages have one static type” is
- formally true
- boring once you understand it
- but the process of understanding it is useful
- not a good argument against dynamic typing
- PL’s version of “is an X a sandwich?”
4
5
101
Conversation
Something I haven’t seen addressed — aren’t statically typed languages unityped, but in the metalanguage? We define type structure via context free grammars, which are de facto recursive sum types.
2
3
I think you're confusing two separate issues. We also use CFGs to define the term grammar, so that on its own doesn't imply unitypedness. Some (but not all) statically typed languages *are* unikinded, though -- kinds being to types what types are to terms.
1
4
Ah, I was misreading the parent comment as s/type structure/term structure/. Like, I think it's funny how I'm making this dependently typed language, but hidden inside is this dynamically typed interpreter.