Impredicativity in Ur/Web

From Impredicative Wiki
Revision as of 14:50, 4 December 2010 by Karn Kallio (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

The Ur/Web type system embeds System F and thus includes impredicative polymorphism.

Here is a simple demonstration of Girard encoding the Boolean and Natural types in Ur/Web.

(* Booleans *)

con gbool :: Type = t :: Type -> (t -> t -> t)

val btrue : gbool = fn [t :: Type] (x : t) (y : t) => x
val bfalse : gbool = fn [t :: Type] (x : t) (y : t) => y

val bnot : gbool -> gbool = fn (b : gbool) [t :: Type] (x : t) (y : t) => b [t] y x  

val btofalse : gbool -> gbool = fn (b : gbool) => bfalse  
val btotrue : gbool -> gbool = fn (b : gbool) => btrue  

val band : gbool -> gbool -> gbool = fn (bx : gbool) (by : gbool) [t :: Type] (x : t) (y : t) => (bx [gbool] by bfalse) [t] x y 
val bor : gbool -> gbool -> gbool = fn (bx : gbool) (by : gbool) [t :: Type] (x : t) (y : t) => (bx [gbool] btrue by) [t] x y 

val bnottrue : gbool = bnot btrue

(* Naturals *)

con gnat :: Type = t :: Type -> ((t -> t) -> t -> t)

val nzero : gnat = fn [t :: Type] (g : t -> t) (x : t) => x
val nsucc : gnat -> gnat = fn (n : gnat) [t :: Type] (g : t -> t) (x : t) => g (n [t] g x)

val nadd : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => nx [t] g (ny [t] g x)
val nadd' : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => (nx [gnat] nsucc ny) [t] g x 

val nmul : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => nx [t] (ny [t] g) x
val nmul' : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => (nx [gnat] (nadd' ny) nzero) [t] g x

val none : gnat = nsucc nzero
val ntwo : gnat = nsucc none
val nthree : gnat = nsucc ntwo

val nsix : gnat = nmul ntwo nthree

(* Predicate *)

val nzerop : gnat -> gbool = fn (n : gnat) => n [gbool] btofalse btrue


fun main () = return <xml>
  <head>
    <title>Impredicativity in Ur/Web</title>
  </head>
  <body>
    <h1>Impredicativity in Ur/Web</h1>
    <p>
      Here we use the System F at the Ur/Web value/type level to
      Girard encode some basic datatypes.
    </p>
    <h2>Illustracion of bnottrue acting on integers</h2>
    <p>
      bnottrue [int] 8 11 = {[bnottrue [int] 8 11]}
    </p>
    <h2>Illustracion of nsix in action over a base type of strings</h2>
    <p>
      {[nsix [string] (strcat "Yay! ") "for Ur/Web"]}
    </p>
    <h2>Illustracion of zero characteristic predicate in action over strings</h2>
    <p>
      nzerop ntwo [string] ''true'' ''false'' = {[nzerop ntwo [string] "true" "false"]}
    </p>
  </body>
</xml>
Personal tools