Giter Site home page Giter Site logo

ttie's Introduction

TTIE - Type Theory with Indexed Equality

A demo interpreter and type checker of a type theory with interval indexed equality types.

The indexed equality type looks like this (in Agda notation):

data Interval : Type where
  0 : Interval
  1 : Interval
  01 : 0 == 1

data Eq (A : Interval -> Type) (A 0) (A 1) : Type where
  refl : (x : (i : Interval) -> A i) -> Eq A (x 0) (x 1)

We write the binders for intervals as a subscript, so Eq_i (A i) x y.

Syntax

The syntax is modeled after Agda and Haskell:

-- a comment
{- also a comment -}
variable
_                     -- a hole, filled in by unification

Type : Type1          -- the type of types

tt : Unit             -- built in unit type, with constructor tt

Unit -> Unit          -- function type
Unit → Unit           -- Unicode
(A : Type) -> A -> A  -- dependent function type
{A : Type} -> A -> A  -- implicit arguments
forall x -> B x       -- the same as (x : _) -> B x
∀ x. B x              -- the same
\x -> e               -- lambdas / anonymous functions
\(x : A) -> e         -- with type annotation
(x : A) => e          -- same
f x                   -- function application
f {x}                 -- explicit application to an implicit argument

(x : A) * B x         -- dependent sums (pairs)
{x : A} * B x         -- with implicit arguments (to model existentials)
exists x -> B x       -- the same as (x : _) * B x
∃ x. B x              -- the same
x , y                 -- construct a pair
proj1 x               -- first projection of a pair
proj2 x               -- second projection
{proj1} x             -- projection of an implicit pair/existential
{x} , y               -- explicit construction of an implicit pair

0
1 : Interval          -- The interval has values 0 and 1
01 : Eq _ 0 1         -- the path between 0 and 1
refl_i i              -- the same
iflip i               -- sends 0 to 1 and vice-versa
~i                    -- the same
iand i j              -- 1 if i and j are both 1
i && j                -- the same
i || j                -- 1 if i or j is 1

Eq A x y              -- type of equality proofs of x and y of type A
Eq_i (A i) x y        -- indexed equality between x : A 0 and y : A 1
x == y                -- sugar for equality type
refl x                -- reflexivity at x
refl_i (x i)          -- indexed version
xy^i                  -- end point of a path, if xy : Eq _ x y, xy^0 = x, xy^1 = y, refl_i xy^i = xy
iv x y xy i           -- desugared version of xy^i

cast_i (A i) u v x    -- substitution: if (x : A u), the result has type (A v)
fw_i (A i) x          -- short hand notation for cast_i (A i) 0 1
bw_i (A i) x          -- short hand notation for cast_i (A i) 1 0

data{left:A; right:B} -- A sum type, constructors have a single argument type
value left x          -- A value of the above data type, you may need a type signature
case x of {left y -> ..; right y -> ..} -- case analysis of a sum type
data{}                -- The type with no constructors (bottom)

Declarations and commands look like

name : Type
name arguments = expression

:help
:quit
:type e
:eval e
:nf e
:check e = e'

Remarks:

  • Built in names like Eq, proj1, cast, etc. must always be fully applied.
  • Spaces around operators like -> are usually required, because - can be part of a name.
  • There is no support for recursion yet.
  • Implicit projections have not yet been implemented.
  • Unification is often not very smart.

Usage

The implementation comes with a REPL and an interpreter:

$ cabal build
$ dist/ttie examples/Lemmas

The unit tests from Tests.hs are also instructive

$ cabal test

Examples

Here is a proof that fw ∘ bw = id

A : Type
B : Type
AB : Eq _ A B
lemma : forall x. fw_i (AB^i) (bw_i AB^i x) == x
lemma = \x -> refl_j (cast_i AB^i j 1 (cast_i AB^i 1 j x))

Proof of function extensionality:

ext : ∀ {A : Type} {B : A → Type} {f g : (x : A) → B x} → (∀ x. f x == g x) → f == g
ext = \fg → refl_i \x → (fg x)^i

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.