1. What is a dependent type 1. ADT -- the simplest dependent-type 2. Singleton types 3. Branding: type proxies 2. Lightweight static capabilities 1. Abstract and Introduction 2. Formalization and proofs 3. Accompanying source code 3. The question of verification 4. Genuine Dependent-type systems This is a joint work with Chung-chieh Shan. We describe several approaches to lightweight dependent-type programming, letting us gain experience with dependent types on existing programming language systems All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time. ``This much is clear: many programmers are already finding practical uses for the approximants to dependent types which mainstream functional languages (especially Haskell) admit, by hook or by crook.''
Idris is an experimental language with full dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. The aims of the project are: * To provide a platform for realistic programming with dependent types. By realistic, we mean the ability to interact with the outside world and use primitive types and operations. This includes networking, file handling, concurrency, etc. * To show that full dependent types do not mean we have to abandon the functional style we have come to know and love with languages like Haskell and OCaml. lightweight dependently typed programming means allowing the programmer full access to values in types, and letting the type checker do the hard work so you don't have to! Future plans include some more useful syntax (local definitions/where clauses being the most important), a compiler,
au:chlipala Ur introduces richer type system features into FP. Ur is functional, pure, statically-typed, and strict. Ur supports metaprogramming based on row types. Ur/Web is standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs "don't go wrong" in a very broad sense. They also may not: * Suffer from any kinds of code-injection attacks * Return invalid HTML * Contain dead intra-application links * Have mismatches between HTML forms and the fields expected by their handlers It is also possible to use metaprogramming to build significant application pieces by analysis of type structure - demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The Ur/Web compiler also produces very efficient object code that does not use gc
Efficiently translating Haskell to JVM Bytecode using GHC's intermediate language, STG. LambdaVM is the proof that complete and efficient translation is possible. LambdaVM is a set of patches to GHC's which extend it to fully support generating useable JVM bytecode. It modifies the three primary components of GHC: * The compiler itself: The compiler has been modified to transform STG, one of GHC's many intermediate languages, to JVM bytecode. * The runtime system (RTS): GHC's RTS implemented as a mix of C and C-- has been reimplemented in Java. * The base libraries: GHC's base libraries have been modified to run on top of Java's standard libraries rather than ANSI C/POSIX libraries. October, 2008 Update LambdaVM is coming back! I've fixed all the GHC 6.8.x build problems and the instructions below should once again work. LambdaVM itself is still based on a circa November, 2007 GHC HEAD but moving all my changes to the current HEAD is next