uAgda 1.0.0.1 → 1.0.0.2

raw patch · 4 files changed

+93/−2 lines, 4 files

Files

• tutorial/02.1-Relevance.ua +61/−0
• tutorial/03-Parametricity.ua +3/−1
• tutorial/03.1-Parametricity-Use.ua +26/−0
• uAgda.cabal +3/−1

@@ -0,0 +1,61 @@+-- Relevance levels and erasure+---------------------------------++-- In uAgda, each term can exist at a specific relevance. +-- +-- For example * is the most relevant level, *< is less relevant, etc.+-- +-- The idea is that a term less relevant worlds can be erased, and the+-- terms remains meaningful.+++-- For example, we can use a more precise type of the Leibniz equality+-- that says that the actual type used is irrelevant for the predicate:++Eq = \ A a b -> (P : A -> *) -> P a -> P b+     : (A : *<) -> (a b : A) -> *1,++-- Another example is the following: the inductive principle for+-- natural numbers is independent on the actual representation of the+-- naturals, so they are irrelevant.  This can be expressed as+-- follows:++-- We assume an (abstract) representation N of naturals, in a less+-- relevant world, as well as constructors for successor and zero.++Nat = \(N : *<) (s : N -> N) (z : N) ->++-- Then define the induction principle as normal (the predicate is in *)+\(n : N) -> (P : N -> *) -> P z -> ((m : N) -> P m -> P (s m)) -> P n,+++-- We know that all the programs we have written using naturals+-- satisfying the above induction principle can be represented by+-- Naturals where the irrelevant parts are erased. We can access this+-- erasure within uAgda by using the % operator. The second argument+-- is the first world of relevance to erase (all less relevant worlds+-- will be erased as well).++Nat-representation = Nat % 1,++-- The normal form of the above term reveals that the result is the+-- usual Church encoding for naturals.+++-- Each term can be copied to a less relevant world:++shiftType = \A -> A<+          : * -> *<,++shiftValue +  = \ A a -> a<+  : (A : *) -> (a : A) -> A<,+++-- In summary, occurences of the < operator can be understood as+-- relevance annotations. They can be used mark types, terms and their+-- usage as irrelevant. They are useful for erasure, but may be safely+-- ignored otherwise.+++*

@@ -33,9 +33,11 @@ -- parametricity and erasure. See the following reference for -- the explanation: --- https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466+-- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466  fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),++   *)

@@ -0,0 +1,26 @@+-- let's use parametricity in a useful way: prove that any+-- function of type (X : *) -> X -> X is the identity.++-- To simplify the example we use impredicativity here, use+-- the -I flag to enable it.++Eq = \A a b -> (P : A -> *) -> P a -> P b+   : (A : *<) -> A -> A -> *+   ,++Theorem = +  (f : (A : *) -> A -> A) ->+  (A : *) ->+  (x : A) ->+  Eq A< x< (f A x)<,+++proof = \(f : (A : *) -> (a : A) -> A) ->+        \(A : *) ->+        \(x : A) -> f! A< (Eq A< x<) x< (\_ p -> p)+      : Theorem+++,+* +

@@ -1,5 +1,5 @@ name:           uAgda-version:        1.0.0.1+version:        1.0.0.2 category:       Dependent Types synopsis:       A simplistic dependently-typed language with parametricity. description:@@ -28,7 +28,9 @@      tutorial/00-Start-Here.ua      tutorial/01-Module.ua      tutorial/02-Holes.ua+     tutorial/02.1-Relevance.ua      tutorial/03-Parametricity.ua+     tutorial/03.1-Parametricity-Use.ua      tutorial/04-Data.ua