Hacker News new | comments | show | ask | jobs | submit login

There's just a different set of terms used here.

In static typing context, "types" is a lexical construct of subexpressions. In this context, dynamically typed languages are "untyped" or "unityped" (one type for all expressions).

In dynamic typing context, "types" are the runtime tags of data with rules about dispatch and what kinds of tags are allowed with what operations.

I think for the benefit of communication, we should refer to the static, compile-time annotation on sub-expressions as "types", and the entity dynamic languages calls "types" as "tags".

Your example:

> More complex analysis requires more and more annotations to specify the contracts of the methods. An example is a C function which takes a char* and an int. You want to annotate that the int indicates the length of the char* buffer, and have a static analyzer enforce that

This is of course certainly compatible with types. Something like:

    func : (n : Int) -> Ptr (Array n Char) -> ...
This is the type of the contract you specified.

Static types and static analysis are basically variants on the same idea. However, static types is part of the ordinary workflow, and static analysis is often treated as an "after-the-fact" feature. This will not work as well, since much of the power of types relates to techniques to structure our programs so that types cover as much as possible.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact