Schlagwort-Archiv: Typentheorie

Functions are Data.

Defunctionalize the Continuation!

James Koppel: The Best Refactoring You've Never Heard Of

Stynamic Hype.

A static type system is a mechanism by which a compiler examines source code and assigns labels (called “types”) to pieces of the syntax, and then uses them to infer something about the program’s behavior. A dynamic type system is a mechanism by which a compiler generates code to keep track of the sort of data (coincidentally, also called its “type”) used by the program. The use of the same word “type” in each of these two systems is, of course, not really entirely coincidental; yet it is best understood as having a sort of weak historical significance. Great confusion results from trying to find a world view in which “type” really means the same thing in both systems.

Chris Smith: What To Know Before Debating Type Systems


A proof assistant is what happens if you spend all your time developing a type checker for your language and forget that programs also need to be run.

Vladislav Zavialov: Why Dependent Haskell is the Future of Software Development

Zombie Code.

Most surprisingly, dead code may affect the result of the program -- even though it is not even executed.

Oleg Kiselyov: Type inference and the undead code

Type Hype.

Functions with two or more arguments of the same type should be forbidden or commutative.

Expected type Target, found Foot.

Informally, though, safe languages can be defined as ones that make it impossible to shoot yourself in the foot while programming.

Benjamin C. Pierce: Types and Programming Languages

Casuality Theory.

There's wisdom in types.

Ältere Beiträge «