The Sage Programming Language

http://sage.soe.ucsc.edu/ https://github.com/ucsc-proglang/sage

A prototype implementation of a language with:

• Executable refinement types
• First-class types (aka full dependent types a la Cayenne)
• Dynamic types (aka gradual typing)

with an implementation supported by:

• An off-the-shelf theorem prover (in this case, hard-coded to Simplify)
• A compile-time interpreter
• A database of run-time failures (every run-time failure occurs "at most once")

Disclaimer: This software is a very rough prototype! It is provided for scientific and pedagogical purposes.

Note: The Simplify binaries included here are not part of the Sage materials. They are distributed for your convenience under the Java Programming Toolkit software license, available at http://www.hpl.hp.com/downloads/crl/jtk/agreement.html

Building and "installing"

Try this

    $ make

If all goes well, you should have a sage executable.

Two copies of the binary executable of the Simplify theorem prover are included. For sage to run correctly (without the -nosimplify flag), an executable named Simplify must exist.

On Linux, the following should work:

  $ ln -s Simplify-1.5.4.linux Simplify

On Windows, this is better:

  cp Simplify-1.5.4.exe.win Simplify.exe

Usage

You can experiment with Sage via its interactive toplevel by running sage with no arguments. We have prepared a tutorial at http://sage.soe.ucsc.edu/tutorial.txt

$ ./sage
creating new database default.db.
     Welcome to Sage

# let x = 3;;
Binding for: x
Type: (Refine Int (fn (x:Int) => (inteq x 3)))
Evaluation: 3

# let add_one (x:Int) = x + 1;;
Binding for: add_one
Type: (x:Int -> (Refine Int (fn (z:Int) => (inteq z (add x 1)))))
Evaluation: (fn (x:Int) => (add x 1))

# add_one 3;;
Type: (Refine Int (fn (z:Int) => (inteq z (add 3 1))))
Evaluation: 4

The fun never ends.

To type check and run a file of sage code, use sage <filename>. A number of example programs are in the tests subdirectory. For example, try sage tests/polylist.f

Running sage -help shows the command-line options, many of which are are for debugging purposes.

Contributors

• Kenn Knowles (@kennknowles)
• Cormac Flanagan
• Stephen Freund
• Jessica Gronski
• Aaron Tomb

Readings

Do you like the ideas in Sage? You may enjoy deep theoretical and practical readings about their development.

The most thorough treatment of the theory, and a good place to jump off to related work, is Kenn's dissertation.

• Executable Refinement Types
  Kenneth Knowles. Doctoral dissertation, 2014.

If you prefer smaller bits, the theory has been published in pieces in conferences and journals over the years.

• Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic
  Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, and Cormac Flanagan.
  Scheme Workshop 2006
• Hybrid type checking
  Kenneth Knowles and Cormac Flanagan
  Transactions on Programming Languages and Systems (TOPLAS) 2010 Revised and extended from Cormac Flanagan's work in Principles of Programming Languages (POPL) 2006
• Hybrid Types, Invariants, and Refinements for Imperative Objects
  Cormac Flanagan, Stephen N. Freund, and Aaron Tomb
  Foundations of Object Oriented Languages (FOOL) 2006
• Type Reconstruction for General Refinement Types
  Kenneth Knowles and Cormac Flanagan
  European Symposium on Programming (ESOP) 2007
• Unifying Hybrid Types and Contracts
  Jessica Gronski and Cormac Flanagan
  Presented at Trends in Functional Programming (TFP) 2007
• Space Efficient Gradual Typing
  Dave Herman, Aaron Tomb, and Cormac Flanagan
  Trends in Functional Programming (TFP) 2007
• Compositional and Decidable Checking for Dependent Contract Types
  Kenneth Knowles and Cormac Flanagan
  Programming Languages meets Program Verification (PLPV) 2009

(It took a few years to discover the name "Executable Refinement Types" but these are all talking about the same sorts of type systems, where the refinements are closely tied to the ability to run-time behavior to enable Hybrid Type Checking)

Other interesting projects

If you are interested in exciting modern developments in refinement types, be sure to check these other projects out!

• Liquid Haskell adds refinement types to Haskell.
• F7 adds refinement types to F#.
• Ynot adds stateful programming capabilities to Coq.
• HCC adds hybrid contract checking to OCaml.

A bit more tangential, but still related, you may also enjoy following the progress of dependently typed programming via Agda, Epigram, Coq, Ur, etc.

Acknowledgments

The example code from Benjamin Pierce's Types and Programming Languages was used with permission as a starting point for this prototype.

License

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.