[antonvs]

Technically, in a type theory context, there’s no such thing as “dynamic typing”. Types are a static, syntactic property of programs.

The correct term for languages that don’t have syntactic types is “untyped”.

> Most people who think they have a problem with dynamic typing actually have a problem with weak typing.

All people who say things like this have never studied computer science.

[_flux]

The term unityped is used as well, and at typing level this also makes sense: you have one type called object, you put that object alongside the value object ("tag"), and then at runtime all operations on that object check if its type object provides the operation the code is trying to apply on it (or maybe each value object directly knows the operations it supports). I think I prefer this term.

"syntactic type" is a weird term to me, though. Is that in common use?

[antonvs]

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