Impredicativity in Ur/Web
From Impredicative Wiki
Revision as of 15:50, 4 December 2010 by Karn Kallio (Talk | contribs)
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>
