1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
| 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 <[email protected]>
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
|