Some Basics on ATS ATS consists of a static component (statics), where types are formed and reasoned about, and a dynamic component (dynamics), where programs are constructed and evaluated. Some Primitive Sorts and Constants The statics of ATS is a simply typed language. The types for terms in the statics are called sorts (so as to avoid potential confusion with the types for terms in the dynamics) and the terms in it are called static terms. We use sigma for sorts and s for static term. The primitive sorts in ATS include bool, int, prop, type, view and viewtype. There are also some primitive constants c in the statics, each of which is assigned a constant sort (or c-sort, for short) of the following form:
A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
Simpler, Easier! In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.) First, the untyped lambda calculus. I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,
ATS is a functional language that supports a variety of advanced types such as dependent types and linear types, and Anairiats is the current implementation of ATS. ATS/Anairiats can run with or without (systematic) garbage collection (GC), and its performance is comparable to imperative languages like C and C++. # File Inclusion # Compilation # The Main Function in ATS # Fixity Declaration # Overloading # Function or Closure? # Variadic Functions # Tail-Recursive Functions # Termination Metrics # Types with Effects # Call-By-Reference # (Persistent) Lists # Linear Lists # Pointers # References # (Persistent) Arrays and Matrices # Linear Arrays # Datatypes # Dataprops # Dataviews # Dataviewtypes # Pattern Matching # Exceptions # Val(ue) and Var(iable) Declarations # Higher-Order Functions # Lazy Evaluation # Macros # Templates # Memory Allocation/Deallocation # Input and Output # Combining ATS and C programs # Programming with Theorem Proving