A type system is a syntactic method for enforcing levels of abstraction in programs. The study of type systems--and of programming languages from a type-theoretic perspective--has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators.
Coming back to the above post by Anton, yes, the kind of runtime type checking exists in lots of popular Java frameworks, even today. And this is where frameworks like Guice and EasyMock really shine with their strongly typed API sets that make you feel more secure within the confines of your IDE and refactoring abilities. The Morale When you are programming in a statically typed language, use appropriate language features to make most of your type checking at compile time. This way, before you hit the run button, you can be assured that your code is well-formed within the bounds of the type system. And you have the power of easier refactoring and cleaner evolution of your codebase.
So why is the restriction imposed? The reasoning behind it is fairly subtle, and is fully explained in the Haskell 98 report. Basically, it solves one practical problem (without the restriction, there would be some ambiguous types) and one semantic problem (without the restriction, there would be some repeated evaluation where a programmer might expect the evaluation to be shared). Those who are for the restriction argue that these cases should be dealt with correctly. Those who are against the restriction argue that these cases are so rare that it's not worth sacrificing the type-independence of eta reduction.
The Curry-Howard correspondence is a mapping between logic and type systems. On the one hand you have logic systems with propositions and proofs. On the other hand you have type systems with types and programs (or functions). As it turns out these two very different things have very similar rules. This article will explore the Curry-Howard correspondence by constructing a proof system using the Haskell type system (how appropriate since Haskell is named after Haskell Curry, the "Curry" in "Curry-Howard"). We'll set up the rules of logic using Haskell types and programs. Then we'll use these rules as an abstract interface to perform some logic profs.
In denotational semantics and functional programming, the terms monad morphism, monad layering, monad constructor, and monad transformer have by now accumulated 20 years of twisted history. The exchange between Eric Kidd and sigfpe about the probability monad prompted me to investigate this history
In a previous post, I wondered about the differences between the thought processes that goes into writing good static code, and those that go into good dynamic code. We figured that there wasn't a lot out there to help dynamic programmers get the hang of static style thinking, so what follows is a simple little toy example, solved in what I think is probably a fairly static typey style.
"Generalized Algebraic Data Structures" have become a a hot new topic. They have recently been added to the GHC compiler. They support the construction, maintenance, and propagation of semantic properties of programs using powerful old ideas about types (the Curry-Howard Isomorphism) in surprisingly easy to understand new ways. The language Omega was designed and implemented to demonstrate their utility. Here a a few talks I gave that explains how they work. Also class lectures
Keywords: Constructive Logic, Type Theory, Category Theory, Lambda calculus, Quantum Computing, Certified Correct Programs main research interest is the application of constructive logic in Computer Science.An example of a constructive logic is Type Theory Type Theory is at the same time a programming language and a logic: propositions correspond to types and proofs to programs. Current research centers on theoretical aspects of Type Theory but also on the construction of elegant and efficient implementations of type theoretic languages. An example of this is the Epigram system, currently under development in Nottingham, which we use to develop programs which are correct by construction. Dr. Altenkirch's research covers applications of Category Theory as a formalism to concisely express abstract properties of mathematical constructions in Computer Science and the investigation of typed lambda calculi as a foundation of (functional) programming languages and Type Theory.
I'm interested in the relative merits of ATS vs. Epigram which is a Pure Type System that seeks to unify types and terms, where ATS distinguishes the statics and dynamics of the language. What benefits and limitations do these approaches have on complexity for both developer and implementor? notes in atsVepig.txt
A type system is a syntactic method for enforcing levels of abstraction in programs. The study of type systems--and of programming languages from a type-theoretic perspective--has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators.
Sage is a prototype functional programming language designed to provide high-coverage checking of expressive program specifications (types). Sage allows a programmer to specify not only simple types such as "Integers" and "Strings" but also arbitrary refinements from simple ranges such as "Positive Integers" to data structures with complex invariants such as "Balanced binary search trees." In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function. Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise The current implementation is a type checker and interpreter for the Sage programming language. Any system with OCaml and GNU Make Sage currently requires the Simplify theorem prover for hybrid type checking.
Adam Chlipala This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. This is the text for a Fall 2008 class at Harvard.
Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program.We describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated as part of the DML project. When used with a simple set of bounds checking qualifiers, Dsolve reduces manual annotation required from 31% of program text to under 1%.
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. This seems like it's related to Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 23-24 of this presentation (PDF). More generally, computation and reflection seem to be gaining recognition as important features for the practical use of Coq Again, the point is to simplify programming with dependent types in Coq
Keywords: Calculus of Constructions, Higher Order Logic, Typed Lambda Calculus, Equational Logic, Rewriting Logic Rewriting logic together with it's membership equational sublogic favors the use of abstract specifications. It has a flexible computation system based on conditional rewriting modulo equations, and via its initial semsntics it supports a very liberal notion of inductive definitions. Pure type systems, on the other hand, in particular the calculus of constructions, provide higher-order (dependent) types, but they are based on a fixed notion of computation, namely beta-reduction. To close this gap we investigate (OCC) an equational variant of the calculus of constructions. The formal executable specification of OCC exploits the reflective capabilities of Maude, yielding an computational efficiency that brings us closer the the goal of a unified tool for programming, specification and verification integrating equational logic, higher-order logic and dependent types.