Impredicativity in Ur/Web
From Impredicative Wiki
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>