Daniel Fridlender Mia Indrika March 2001 Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus
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.
Dependent type systems, in which types can depend on values, admit detailed specifications of function behavior and data invariants. Programming languages based on System F do not have dependent types, and are therefore more limited in what structure or function invariants can be encoded in the type system. In this paper, we show how guarded algebraic datatypes can simulate dependent types. We formalize additions to a guarded-datatypes-enhanced System F that allow types to depend on values and discuss the programming style that results, which is similar to theorem proving. Our technique can be applied to multiple existing programming languages, including Haskell and C#. We also introduce an idiom for eliminating any execution cost from programming with simulated dependent types. We have developed a tool to automatically produce the boilerplate necessary for the simulation, and we have used it to enforce data structure invariants and to allow elision of run-time bounds checks.
Datatype-Generic Programming Roland Backhouse at the University of Nottingham and Jeremy Gibbons at the University of Oxford have a joint EPSRC-supported project entitled Datatype-Generic Programming, running for three years and starting on 1st October 2003. Aim The project is to develop a novel mechanism for parametrizing programs, namely parametrization by a datatype or type constructor. The mechanism is related to parametric polymorphism, but of higher order. We aim to develop a calculus for constructing datatype-generic programs, with the ultimate goal of improving the state of the art in generic object-oriented programming, as occurs for example in the C++ Standard Template Library. further details of the project can be obtained from the contacts listed below.
Research Interests Programming Languages, Logic and Type Theory, Logical Frameworks, Automated Deduction, Trustworthy Computing (see also Publications, Students & Co-authors) Projects Logosphere A Formal Digital Library Triple Type Refinement in Programming Languages ConCert Language Technology for Trustless Software Dissemination Twelf Logical and Meta-Logical Frameworks SeLF Distributed System Security via Logical Frameworks Manifest Security Logics and Languages for Manifestly Secure Systems Prospero Integrating Types and Specifications
The Curry-Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.
popl2008 ** 1. GADTs are syntactic sugar. The real structures at work are existentially quantified types and the equality GADT. 2. Indexing by a set, rather than a category, as GADTs do means that really this is dependently typed programming faked in Haskell by using kind level proxies for types 3. As a result, Haskell ends up with a curious "logic programming" feel to its type level computation and functional programming feel to its term-level computation. PJohann and NGhani ** his main point (which worked with me) is that we should pay more attention Kan extensions. We already know and love (strong) functors, (co)monads, adjunctions and the Yoneda lemma.