FGJω is a language design that extends Featherweight
Generic Java with variables representing type constructors.
Papers
-
Adding Type Constructor Parameterization to Java.
Vincent Cremet and Philippe Altherr.
In Journal of Object Technology, vol. 7,
no. 5, Special Issue: Workshop on FTfJP, ECOOP 07, June 2008, pp.25-65
(http://www.jot.fm/issues/issue_2008_06/article2/),
(pdf),
(bib).
-
A previous
version was presented at the FTfJP'07 ECOOP workshop.
Compiler
- hofgj-compiler.tar.gz
- Archive containing an executable version of our compiler. It
comes with a README explaining its
usage and syntax.
Examples
- Predef.java
- Basic data structures and operations (to be compiled with every other file).
- OOMonads.java
- Library for object-oriented monads.
- GADTs.java
- Implementation of a safe evaluator using generalized algebraic data types.
- UniversalVisitor.java
- Implementation of a safe evaluator using generalized algebraic data types (more general than GADTs.java).
Proofs
The type safety of FGJΩ, a calculus that is more
general than FGJω, has been proven in Coq version 8.2 (August 2009):
(README)
(Download archive)
(Browse definitions and theorems)
The proof was initially released in August 2007 and could be checked
with Coq version 8.0pl3 (Jan 2006):
(Download the old archive)
Related Posts (on the Scala mailing list)
-
Re: expressiveness of abstract types
.
Posted by V. Cremet (June 2005).
- About a translation of Haskell type classes (including the one of monads) in Scala.
-
Re: Scala type system questions -- representing the concept of monads in Scala
.
Posted by P. Altherr (January 2006).
- About an encoding of abstract type constructors in Scala using virtual types. Includes a full example about monads
-
Re: higher-order type variables
.
Posted by V. Cremet (March 2006).
- About an encoding of higher-order type variables in Scala using virtual types.
People
Philippe Altherr received
a Ph.D. in Computer Science from EPFL, Switzerland in 2006. His
research interests include programming language design and compiler
implementation techniques.
Vincent Cremet received a
Ph.D. in Computer Science from EPFL, Switzerland in 2006. His research
interests include the design and formal proof of advanced type systems
for object-oriented languages.