http://www.impredicative.com/wiki/index.php?title=Impredicativity_in_Ur/Web&feed=atom&action=history
Impredicativity in Ur/Web - Revision history
2024-03-29T14:19:15Z
Revision history for this page on the wiki
MediaWiki 1.19.20+dfsg-2.3
http://www.impredicative.com/wiki/index.php?title=Impredicativity_in_Ur/Web&diff=86&oldid=prev
Karn Kallio: A simple demonstration of impredicativity in Ur/Web
2010-12-04T19:50:36Z
<p>A simple demonstration of impredicativity in Ur/Web</p>
<p><b>New page</b></p><div>The Ur/Web type system embeds System F and thus includes impredicative polymorphism.<br />
<br />
Here is a simple demonstration of Girard encoding the Boolean and Natural types in Ur/Web.<br />
<br />
<pre><br />
(* Booleans *)<br />
<br />
con gbool :: Type = t :: Type -> (t -> t -> t)<br />
<br />
val btrue : gbool = fn [t :: Type] (x : t) (y : t) => x<br />
val bfalse : gbool = fn [t :: Type] (x : t) (y : t) => y<br />
<br />
val bnot : gbool -> gbool = fn (b : gbool) [t :: Type] (x : t) (y : t) => b [t] y x <br />
<br />
val btofalse : gbool -> gbool = fn (b : gbool) => bfalse <br />
val btotrue : gbool -> gbool = fn (b : gbool) => btrue <br />
<br />
val band : gbool -> gbool -> gbool = fn (bx : gbool) (by : gbool) [t :: Type] (x : t) (y : t) => (bx [gbool] by bfalse) [t] x y <br />
val bor : gbool -> gbool -> gbool = fn (bx : gbool) (by : gbool) [t :: Type] (x : t) (y : t) => (bx [gbool] btrue by) [t] x y <br />
<br />
val bnottrue : gbool = bnot btrue<br />
<br />
(* Naturals *)<br />
<br />
con gnat :: Type = t :: Type -> ((t -> t) -> t -> t)<br />
<br />
val nzero : gnat = fn [t :: Type] (g : t -> t) (x : t) => x<br />
val nsucc : gnat -> gnat = fn (n : gnat) [t :: Type] (g : t -> t) (x : t) => g (n [t] g x)<br />
<br />
val nadd : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => nx [t] g (ny [t] g x)<br />
val nadd' : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => (nx [gnat] nsucc ny) [t] g x <br />
<br />
val nmul : gnat -> gnat -> gnat = fn (nx : gnat) (ny : gnat) [t :: Type] (g: t -> t) (x : t) => nx [t] (ny [t] g) x<br />
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<br />
<br />
val none : gnat = nsucc nzero<br />
val ntwo : gnat = nsucc none<br />
val nthree : gnat = nsucc ntwo<br />
<br />
val nsix : gnat = nmul ntwo nthree<br />
<br />
(* Predicate *)<br />
<br />
val nzerop : gnat -> gbool = fn (n : gnat) => n [gbool] btofalse btrue<br />
<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Impredicativity in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Impredicativity in Ur/Web</h1><br />
<p><br />
Here we use the System F at the Ur/Web value/type level to<br />
Girard encode some basic datatypes.<br />
</p><br />
<h2>Illustracion of bnottrue acting on integers</h2><br />
<p><br />
bnottrue [int] 8 11 = {[bnottrue [int] 8 11]}<br />
</p><br />
<h2>Illustracion of nsix in action over a base type of strings</h2><br />
<p><br />
{[nsix [string] (strcat "Yay! ") "for Ur/Web"]}<br />
</p><br />
<h2>Illustracion of zero characteristic predicate in action over strings</h2><br />
<p><br />
nzerop ntwo [string] ''true'' ''false'' = {[nzerop ntwo [string] "true" "false"]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>
Karn Kallio