Skip to content

Comment on Borrow-checking without type-checkingparent

Comments

"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...

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.