name: upts
version: 0.1.0
cabal-version: >= 1.6 && < 2
build-type: Simple
license: BSD3
license-file: LICENSE
category: Language
author: Dan Doel
copyright: (c) Dan Doel, 2008-2009
maintainer: Dan Doel
homepage: http://code.haskell.org/~dolio/
stability: experimental
synopsis: An implementation of a pure type system with universe polymorphism.
description: upts provides several modules for working with a type theory
similar to pure type systems. It is based on the pts library
by the same author, but rather than being parameterized by the
axioms to be used, a specific dependent type theory has been
chosen, so that more interesting features can be developed.
.
The type theory in upts has a predicative hierarchy of universes,
Type[i], for each integer i. However, levels are treated as an
ordinary type, and can be quantified over using both Pi and Sigma
types. This enables universe polymorphism, where a single type
definition is able to be used on many levels of the hierarchy. To
avoid paradox (hopefully), universe polymorphic types such as:
(i : Level) -> Type[i]
{ i : Level | Type[i] }
inhabit a 'top' universe, denoted by a capital omega, which cannot
be quantified over. In this manner, it is similar to the lambda
cube, which has values, types, * and [] in its hierarchy, the
last being the top, and not subject to discussion from within the
calculus.
tested-with: GHC == 6.10.3 && == 6.10.4
source-repository head
type: darcs
location: http://code.haskell.org/~dolio/upts/
library
hs-source-dirs: .
ghc-options: -O2 -Wall
extensions: ScopedTypeVariables, PatternGuards, MultiParamTypeClasses
build-depends: base>=4 && < 5, parsec>=3 && < 4, mtl, bound >= 0.4, containers, prelude-extras
exposed-modules: Language.UPTS.SyntaxTree
Language.UPTS.TypeCheck
Language.UPTS.Parser
executable upts-repl
main-is: REPL.hs
build-depends: base==4.*, mtl, haskeline > 0.6 && < 1, bound >= 0.4, containers, prelude-extras
extensions: Rank2Types, ExistentialQuantification,
GeneralizedNewtypeDeriving, PatternGuards
ghc-options: -O2 -Wall