Hacker News new | ask | show | jobs
by antonvs 50 days ago
"Unityped" is informal, and inaccurate in a type theory context. The description you gave refers to the runtime/semantic domain, not to types in the type theory sense.

I used "syntactic type" to underscore that formally, typing is a syntactic system that assigns types to terms, where terms are syntactic expressions.

Because of that, it's usually redundant to include "syntactic". You'll typically see it used when it's being contrasted to some other less standard approach to typing, e.g.: https://blog.sigplan.org/2019/10/17/what-type-soundness-theo...