http://www.impredicative.com/wiki/api.php?action=feedcontributions&user=Karn+Kallio&feedformat=atomImpredicative Wiki - User contributions [en]2024-03-29T06:35:20ZUser contributionsMediaWiki 1.19.20+dfsg-2.3http://www.impredicative.com/wiki/index.php/Basic_Example_of_Type_Classes_as_Predicates_Over_TypesBasic Example of Type Classes as Predicates Over Types2010-12-13T23:36:45Z<p>Karn Kallio: An example of viewing type classes as predicates over types</p>
<hr />
<div>Here is a simple example trying to show how type classes can be viewed as predicates over types.<br />
<br />
<pre><br />
structure Example : sig<br />
type socrates <br />
type alice<br />
type bob<br />
<br />
type trigger<br />
type silver<br />
type hidalgo<br />
<br />
class human<br />
class horse<br />
class mortal<br />
<br />
val human_socrates : human socrates<br />
val human_alice : human alice<br />
val human_bob : human bob<br />
<br />
val horse_trigger : horse trigger<br />
val horse_silver : horse silver<br />
val horse_hidalgo : horse hidalgo<br />
<br />
val humans_mortal : t ::: Type -> human t -> mortal t <br />
end = struct<br />
<br />
(*<br />
* We will make some types to represent objects.<br />
*)<br />
<br />
type socrates = unit<br />
type alice = unit<br />
type bob = unit<br />
<br />
type trigger = unit<br />
type silver = unit<br />
type hidalgo = unit<br />
<br />
(*<br />
* Now we use type classes as predicates over these types.<br />
*)<br />
<br />
class human t = unit<br />
class horse t = unit<br />
class mortal t = unit<br />
<br />
(*<br />
* We use type class instances to say of which types these<br />
* predicates are true.<br />
*)<br />
<br />
val human_socrates : human socrates = () <br />
val human_alice : human alice = () <br />
val human_bob : human bob = () <br />
<br />
val horse_trigger : horse trigger = ()<br />
val horse_silver : horse silver = ()<br />
val horse_hidalgo : horse hidalgo = ()<br />
<br />
(*<br />
* Humans are mortal<br />
*)<br />
fun humans_mortal [t ::: Type] (h : human t) : mortal t = h <br />
end<br />
<br />
open Example<br />
<br />
(*<br />
* The Ur/Web type class facility can check our proof that Socrates is mortal<br />
*)<br />
<br />
val mortal_socrates : mortal socrates = humans_mortal<br />
<br />
(*<br />
* But there is no value we can put on the right to show Hidalgo is mortal<br />
*)<br />
<br />
(* val mortal_hidalgo : mortal hidalgo = () *)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Type Classes as Predicates in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Type Classes as Predicates in Ur/Web</h1><br />
<p><br />
The Ur/Web type class mechanism can represent predicates.<br />
</p><br />
<h2><br />
An illustracion <br />
</h2><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Code_SamplesCode Samples2010-12-13T23:33:03Z<p>Karn Kallio: Added link to type classes as predicates example</p>
<hr />
<div>Here is a list of pages containing samples or demonstrations of Ur/Web code.<br />
<br />
=== Records ===<br />
* [[Using Top.Fold to count fields of a record]]<br />
* [[Polymorphic Variants Usage Example]]<br />
<br />
=== Type Classes ===<br />
* [[Basic Examples of the Type Class Mechanism in Ur/Web]]<br />
* [[Abstract and Concrete Type Classes]]<br />
* [[Basic Example of Type Classes as Predicates Over Types]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Abstract_and_Concrete_Type_ClassesAbstract and Concrete Type Classes2010-12-13T22:29:47Z<p>Karn Kallio: Comparison between an abstract and concrete type class</p>
<hr />
<div>Type classes can be abstract such that new instances may not be added (giving a closed, fixed predicate of general arity over types) or concrete with the possibility of users adding new types to the family (extending the extension of the predicate).<br />
<br />
Here is a sample of an abstract type class.<br />
<br />
<pre><br />
(*<br />
* Here is an abstract type class example. We cannot add more instances.<br />
*)<br />
<br />
structure Abstract : sig<br />
class abs<br />
val speak : t ::: Type -> abs t -> t -> string<br />
<br />
val abs_int : abs int<br />
val abs_float : abs float<br />
end = struct<br />
class abs t = t -> string<br />
<br />
fun speak [t ::: Type] (d : abs t) (x : t) = d x<br />
<br />
fun abs_int (i : int) = "integer noise"<br />
fun abs_float (f : float) = "float noise"<br />
end<br />
<br />
open Abstract<br />
<br />
(*<br />
* If we try to make a string speak we will get an error.<br />
* There is no instance for string in the class abs.<br />
*)<br />
<br />
(* val s : string = speak "What noise does a string make?" *)<br />
<br />
(*<br />
* We can think of the functions abs_int and abs_float being "evidence" witnessing<br />
* the fact that the types int and float belong to the class abs ... if we think<br />
* of abs as being a one-place predicate over types then its extension or characteristic<br />
* set holds int and float<br />
*)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Concrete and Abstract Type Classes in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Concrete and Abstract Type Classes</h1><br />
<p><br />
The Ur/Web type class mechanism allows for both concrete and abstract classes.<br />
</p><br />
<h2><br />
An illustracion <br />
</h2><br />
<p><br />
Some integer noises speak 3 = {[speak 3]} speak 8 = {[speak 8]} <br />
</p><br />
<p><br />
Some float noises speak 5.4 = {[speak 5.4]} speak 3.14 = {[speak 3.14]}<br />
</p><br />
</body><br />
</xml><br />
</pre><br />
<br />
Here is a sample of a concrete type class.<br />
<br />
<pre><br />
(*<br />
* Extending a concrete type class in Ur/Web<br />
*)<br />
<br />
structure Concrete : sig<br />
class conc<br />
<br />
val speak : t ::: Type -> conc t -> t -> string<br />
<br />
val mkConc : t ::: Type -> (t -> string) -> conc t<br />
<br />
val conc_int : conc int<br />
val conc_float : conc float<br />
end = struct<br />
class conc t = t -> string<br />
<br />
fun speak [t ::: Type] (d : conc t) (x : t) = d x<br />
<br />
fun mkConc [t ::: Type] (f : t -> string) = f<br />
<br />
fun conc_int (i : int) = "makes an integer noise"<br />
fun conc_float (f : float) = "makes a float noise"<br />
end<br />
<br />
(*<br />
* The presence of mkConc among the items exported by the<br />
* Concrete module is what makes the conc typeclass concrete.<br />
* At the Ur/Web module system or typeclass system there is no<br />
* distinction between these cases via different constructs.<br />
* Now users may add their own instances.<br />
*)<br />
<br />
open Concrete<br />
<br />
(* We add a string case *)<br />
<br />
val conc_string : conc string = mkConc (fn (s : string) => "makes a string noise")<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Concrete and Abstract Type Classes in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Concrete and Abstract Type Classes</h1><br />
<p><br />
The Ur/Web type class mechanism allows for both concrete and abstract classes.<br />
</p><br />
<h2><br />
An illustracion <br />
</h2><br />
<p><br />
Some integer noises speak 3 = {[speak 3]} speak 8 = {[speak 8]} <br />
</p><br />
<p><br />
Some float noises speak 5.4 = {[speak 5.4]} speak 3.14 = {[speak 3.14]}<br />
</p><br />
<p><br />
Some string noises speak "aaa" = {[speak "aaa"]} speak "foo" = {[speak "foo"]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Code_SamplesCode Samples2010-12-13T22:23:32Z<p>Karn Kallio: Added link to concrete vs abstract type classes page</p>
<hr />
<div>Here is a list of pages containing samples or demonstrations of Ur/Web code.<br />
<br />
=== Records ===<br />
* [[Using Top.Fold to count fields of a record]]<br />
* [[Polymorphic Variants Usage Example]]<br />
<br />
=== Type Classes ===<br />
* [[Basic Examples of the Type Class Mechanism in Ur/Web]]<br />
* [[Abstract and Concrete Type Classes]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Basic_Examples_of_the_Type_Class_Mechanism_in_Ur/WebBasic Examples of the Type Class Mechanism in Ur/Web2010-12-12T16:48:18Z<p>Karn Kallio: Clarification between constraint and polymorphism</p>
<hr />
<div>Ur/Web permits regulated ad hoc polymorphism via a type class mechanism.<br />
Here are some simple example usages.<br />
<br />
<pre><br />
(*<br />
* Here is some simple examples of the typeclass facility in Ur/Web.<br />
* Note that classes are not available in the module which defines them,<br />
* so to make the examples work they may not be at the top level.<br />
*)<br />
<br />
structure Measurable : sig<br />
class measurable<br />
<br />
val length : t ::: Type -> measurable t -> t -> int<br />
<br />
val measurable_string : measurable string<br />
val measurable_list : t ::: Type -> measurable t -> measurable (list t)<br />
end = struct<br />
class measurable :: Type -> Type = fn (t :: Type) => t -> int<br />
<br />
val length : t ::: Type -> measurable t -> t -> int = fn [t ::: Type] (m : measurable t) => m<br />
<br />
val measurable_string : measurable string = strlen<br />
<br />
(* Here we copy listlength for sake of a self-contained example, but it is in the<br />
* library as List.length; you can get it by $/list<br />
*)<br />
<br />
val listlength = fn [a] =><br />
let<br />
fun length' acc (ls : list a) =<br />
case ls of<br />
[] => acc<br />
| _ :: ls => length' (acc + 1) ls<br />
in<br />
length' 0<br />
end<br />
<br />
val measurable_list : t ::: Type -> measurable t -> measurable (list t) = fn [t ::: Type] (m : measurable t) => listlength<br />
end<br />
<br />
open Measurable<br />
<br />
(* <br />
* These will not compile because there is no instance for these types in the class<br />
*)<br />
<br />
(*<br />
val i : int = length 7<br />
val i : int = length (1 :: 3 :: 9 :: [])<br />
*)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Type Classes in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Type Classes</h1><br />
<p><br />
Ur/Web includes a type class mechanism for controlling ad hoc polymorphism.<br />
</p><br />
<h2><br />
An illustracion of the Measurable class on strings and lists.<br />
</h2><br />
<p><br />
Here we see length "Ur/Web" = {[length "Ur/Web"]}<br />
</p><br />
<p><br />
Here we see length ("a" :: "b" :: "C" :: []) = {[length ("a" :: "b" :: "C" :: [])]}<br />
</p><br />
</body><br />
</xml><br />
</pre><br />
<br />
We can have instances polymorphic over the type held in our lists.<br />
<br />
<pre><br />
(*<br />
* Type class polymorphic over type of list<br />
*)<br />
<br />
structure Measurable : sig<br />
class measurable<br />
<br />
val length : t ::: Type -> measurable t -> t -> int<br />
<br />
val measurable_list : t ::: Type -> measurable (list t)<br />
end = struct<br />
class measurable t = t -> int<br />
<br />
val length : t ::: Type -> measurable t -> t -> int = fn [t ::: Type] (m : measurable t) => m<br />
<br />
(*<br />
* Here we copy listlength for sake of a self-contained example, but it is in the<br />
* library as List.length; you can get it by $/list<br />
*)<br />
<br />
val listlength = fn [a] =><br />
let<br />
fun length' acc (ls : list a) =<br />
case ls of<br />
[] => acc<br />
| _ :: ls => length' (acc + 1) ls<br />
in<br />
length' 0<br />
end<br />
<br />
val measurable_list : t ::: Type -> measurable (list t) = fn [t ::: Type] => listlength<br />
end<br />
<br />
open Measurable<br />
<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Type Classes in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Type Classes</h1><br />
<p><br />
Ur/Web includes a type class mechanism for controlling ad hoc polymorphism.<br />
</p><br />
<h2><br />
An illustracion of the Measurable class polymorphic over lists.<br />
</h2><br />
<p><br />
Here we see length ("a" :: "b" :: "C" :: []) = {[length ("a" :: "b" :: "C" :: [])]}<br />
</p><br />
<p><br />
Here we see length (1 :: 2 :: 8 :: 2 :: []) = {[length (1 :: 2 :: 8 :: 2 :: [])]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Basic_Examples_of_the_Type_Class_Mechanism_in_Ur/WebBasic Examples of the Type Class Mechanism in Ur/Web2010-12-12T15:35:11Z<p>Karn Kallio: Simple usage example of the type class facility</p>
<hr />
<div>Ur/Web permits regulated ad hoc polymorphism via a type class mechanism.<br />
Here are some simple example usages.<br />
<br />
<pre><br />
(*<br />
* Here is some simple examples of the typeclass facility in Ur/Web.<br />
* Note that classes are not available in the module which defines them,<br />
* so to make the examples work they may not be at the top level.<br />
*)<br />
<br />
structure Measurable : sig<br />
class measurable<br />
<br />
val length : t ::: Type -> measurable t -> t -> int<br />
<br />
val measurable_string : measurable string<br />
val measurable_list : t ::: Type -> measurable t -> measurable (list t)<br />
end = struct<br />
class measurable :: Type -> Type = fn (t :: Type) => t -> int<br />
<br />
val length : t ::: Type -> measurable t -> t -> int = fn [t ::: Type] (m : measurable t) => m<br />
<br />
val measurable_string : measurable string = strlen<br />
<br />
(* Here we copy listlength for sake of a self-contained example, but it is in the<br />
* library as List.length; you can get it by $/list<br />
*)<br />
<br />
val listlength = fn [a] =><br />
let<br />
fun length' acc (ls : list a) =<br />
case ls of<br />
[] => acc<br />
| _ :: ls => length' (acc + 1) ls<br />
in<br />
length' 0<br />
end<br />
<br />
val measurable_list : t ::: Type -> measurable t -> measurable (list t) = fn [t ::: Type] (m : measurable t) => listlength<br />
end<br />
<br />
open Measurable<br />
<br />
(* <br />
* These will not compile because there is no instance for these types in the class<br />
*)<br />
<br />
(*<br />
val i : int = length 7<br />
val i : int = length (1 :: 3 :: 9 :: [])<br />
*)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Type Classes in Ur/Web</title><br />
</head><br />
<body><br />
<h1>Type Classes</h1><br />
<p><br />
Ur/Web includes a type class mechanism for controlling ad hoc polymorphism.<br />
</p><br />
<h2><br />
An illustracion of the Measurable class on strings and lists.<br />
</h2><br />
<p><br />
Here we see length "Ur/Web" = {[length "Ur/Web"]}<br />
</p><br />
<p><br />
Here we see length ("a" :: "b" :: "C" :: []) = {[length ("a" :: "b" :: "C" :: [])]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Code_SamplesCode Samples2010-12-12T15:33:26Z<p>Karn Kallio: Add section for type classes</p>
<hr />
<div>Here is a list of pages containing samples or demonstrations of Ur/Web code.<br />
<br />
=== Records ===<br />
* [[Using Top.Fold to count fields of a record]]<br />
* [[Polymorphic Variants Usage Example]]<br />
<br />
=== Type Classes ===<br />
* [[Basic Examples of the Type Class Mechanism in Ur/Web]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Polymorphic_Variants_Usage_ExamplePolymorphic Variants Usage Example2010-12-10T00:20:40Z<p>Karn Kallio: Sample usage of polymorphic variants</p>
<hr />
<div>The Ur/Web record calculus contains polymorphic variants. Below is a small example of usage of make and match, as well as a little discussion.<br />
<br />
<pre><br />
(* Given a row type there are two associated types: record types and variant types. *)<br />
<br />
(* Starting with the row type rr *)<br />
<br />
con rr :: {Type} = [Foo = int, Bar = string]<br />
<br />
(* we can make a record type codatarr (using $) or a variant type datarr (using variant) *)<br />
<br />
con codatarr :: Type = $rr<br />
con datarr :: Type = variant rr<br />
<br />
(* The record type codatarr describes codata; values of type $rr can be broken down into<br />
* their components. Each value of type codatarr must accept both the destructors<br />
* Foo and Bar, returning values that are ints or strings respectively.<br />
*<br />
* The variant type datarr describes data; values of type variant rr can be built from<br />
* components. Each value of type datarr has been made by applying either the Foo or Bar<br />
* constructor to an int or string respectively.<br />
*)<br />
<br />
(* Ur/Web also permits the construction of data types via the datatype declaration.<br />
* Here is a sample showing usage of variants with the algebraic datatype parallel.<br />
*)<br />
<br />
(* Let us make a variant type of playing card suits. *)<br />
<br />
con cardsuits :: {Unit} = [Club, Diamond, Heart, Spade]<br />
con cardsuit :: Type = variant (mapU unit cardsuits)<br />
<br />
(* We can make the parallel algebraic datatype *)<br />
<br />
datatype cardsuitalg = Club | Diamond | Heart | Spade<br />
<br />
(* Here is a diamond *)<br />
<br />
val diamond = make [#Diamond] ()<br />
val diamond' = Diamond<br />
<br />
(* Here is how to match by cases on a variant *)<br />
<br />
val namecase = {Club = (fn (_ : unit) => "club"),<br />
Diamond = (fn (_ : unit) => "diamond"),<br />
Heart = (fn (_ : unit) => "heart"),<br />
Spade = (fn (_ : unit) => "spade")}<br />
<br />
val diamondname = match diamond namecase<br />
<br />
(* The algebraic version could be like this *)<br />
<br />
fun cardname card =<br />
case card of<br />
Club => "club"<br />
| Diamond => "diamond"<br />
| Heart => "heart"<br />
| Spade => "spade"<br />
<br />
val diamondname' = cardname diamond'<br />
<br />
(* Now let us show polymorphism. We make two variant types sharing a constructor Medium *)<br />
<br />
con temps :: {Unit} = [Hot, Medium, Cold]<br />
con temp :: Type = variant (mapU unit temps)<br />
<br />
con sizes :: {Unit} = [Large, Medium, Small]<br />
con size :: Type = variant (mapU unit sizes)<br />
<br />
val tempcase = {Hot = (fn (_ : unit) => 10),<br />
Medium = (fn (_ : unit) => 5),<br />
Cold = (fn (_ : unit) => 1)}<br />
<br />
val sizecase = {Large = (fn (_ : unit) => 8),<br />
Medium = (fn (_ : unit) => 4),<br />
Small = (fn (_ : unit) => 2)}<br />
<br />
(* Here medium1 and medium2 have undetermined types; polymorphic variants mean the types will<br />
* be determined according to the usage *)<br />
<br />
val medium1 = make [#Medium] ()<br />
val medium2 = make [#Medium] ()<br />
<br />
(* This usage allows type unification *)<br />
<br />
val mediumtemp = match medium1 tempcase<br />
val mediumsize = match medium2 sizecase<br />
<br />
(* Now let us try via datatype declaration. Here are two algebraic datatypes sharing the Medium constructor *)<br />
<br />
datatype temp = Hot | Medium | Cold<br />
datatype size = Large | Medium | Small<br />
<br />
(* What type will the values constructed by Medium have? *)<br />
<br />
(* The commented out functions below do not compile .. the Medium constructor is not polymorphic;<br />
* it must "decide" on one of temp or size type<br />
*)<br />
<br />
(*<br />
fun tempvalue temp =<br />
case temp of<br />
Hot => 10<br />
| Medium => 5<br />
| Cold => 1<br />
<br />
fun sizevalue size =<br />
case size of<br />
Large => 8<br />
| Medium => 4<br />
| Small => 2<br />
*)<br />
<br />
(* The novelty of polymorphic variants over algebraic datatypes is that with polymorphic variants<br />
* it is possible to express values with partial types *)<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Variant types</title><br />
</head><br />
<body><br />
<h1>Variant Types</h1><br />
<p><br />
The Ur/Web record calculus includes variant types.<br />
</p><br />
<p><br />
diamondname = {[diamondname]} <br/><br />
diamondname' = {[diamondname']} <br/><br />
mediumtemp = {[mediumtemp]} <br/><br />
mediumsize = {[mediumsize]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Code_SamplesCode Samples2010-12-10T00:17:04Z<p>Karn Kallio: Added link to polymorphic variants usages page</p>
<hr />
<div>Here is a list of pages containing samples or demonstrations of Ur/Web code.<br />
<br />
=== Records ===<br />
* [[Using Top.Fold to count fields of a record]]<br />
* [[Polymorphic Variants Usage Example]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Using_Top.Fold_to_count_fields_of_a_recordUsing Top.Fold to count fields of a record2010-12-08T15:04:51Z<p>Karn Kallio: Fixed missing pre tag</p>
<hr />
<div>This code example shows a use of Top.Fold to count the fields of a type level record.<br />
<br />
<pre><br />
con rr :: {Type} = [One = int, Two = string, Three = bool, Four = list float] <br />
<br />
val q : int = @@fold [fn (rx :: {Type}) => (int)]<br />
(fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] acc => 1 + acc)<br />
(0) [rr] (_ : folder rr)<br />
<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Count fields of a record type</title><br />
</head><br />
<body><br />
<h1>Count fields of a record type</h1><br />
<p><br />
We can use fold to count the fields in a type level record.<br />
</p><br />
<p><br />
Here is the value of q: {[q]}<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Using_Top.Fold_to_count_fields_of_a_recordUsing Top.Fold to count fields of a record2010-12-08T15:04:18Z<p>Karn Kallio: Demonstration of Top.fold usage to count record type fields</p>
<hr />
<div>This code example shows a use of Top.Fold to count the fields of a type level record.<br />
<br />
con rr :: {Type} = [One = int, Two = string, Three = bool, Four = list float] <br />
<br />
val q : int = @@fold [fn (rx :: {Type}) => (int)]<br />
(fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] acc => 1 + acc)<br />
(0) [rr] (_ : folder rr)<br />
<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Count fields of a record type</title><br />
</head><br />
<body><br />
<h1>Count fields of a record type</h1><br />
<p><br />
We can use fold to count the fields in a type level record.<br />
</p><br />
<p><br />
Here is the value of q: {[q]}<br />
</p><br />
</body><br />
</xml></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Code_SamplesCode Samples2010-12-08T14:59:14Z<p>Karn Kallio: Make directory page to list code samples</p>
<hr />
<div>Here is a list of pages containing samples or demonstrations of Ur/Web code.<br />
<br />
=== Records ===<br />
* [[Using Top.Fold to count fields of a record]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/UrUr2010-12-08T14:55:36Z<p>Karn Kallio: Added link to code samples list page</p>
<hr />
<div>[http://www.impredicative.com/ur/ Project web site]<br />
<br />
=== Topics ===<br />
* [[contributing to this wiki]]<br />
* [[Ur C FFI Example|C FFI Example]]<br />
* [[Ur Performance Comparisons|Performance Comparisons]]<br />
* [[Ur FAQ|Ur FAQ]]<br />
* [http://github.com/MarcWeber/vim-addon-urweb minimal Vim support]<br />
* [[companies supporting the urweb language]]<br />
* [[Impredicativity in Ur/Web]]<br />
* [[Expressing subrecord constraints]]<br />
* [[Libraries and FFI bindings]]<br />
* [[Code Samples]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Expressing_subrecord_constraintsExpressing subrecord constraints2010-12-08T02:05:24Z<p>Karn Kallio: Expression of record subtyping in terms of disjointness and symmetric concatenation.</p>
<hr />
<div>It is possible to use the disjointness constraints [a ~ b] and symmetric concatenation a ++ b of the Ur/Web record calculus to express record subtype constraints.<br />
<br />
<pre><br />
(* Here the Ur/Web compiler infers the evidence ( the "extension" below ) which shows the value x has a record subtype of super *)<br />
fun subrecordWitness [super :: {Type}] [extension ::: {Type}] [super ~ extension] (fl : folder super) (x : $(super ++ extension))<br />
= @@fold [fn (r :: {Type}) => [r ~ extension] => $(r ++ extension) -> $r]<br />
(fn [nm :: Name] [t :: Type] [r :: {Type}] [[nm] ~ r] (acc : [r ~ extension] => $(r ++ extension) -> $r) <br />
[[nm = t] ++ r ~ extension] => fn (rn : $([nm = t] ++ r ++ extension)) => {nm = rn.nm} ++ acc(rn -- nm))<br />
(fn [[] ~ extension] (x : $extension) => {}) [super] fl ! x<br />
<br />
con supertype :: {Type} = [One = string, Two = int]<br />
<br />
val v : $supertype = subrecordWitness [supertype] {One = "foo", Two = 2, Three = "bar"}<br />
<br />
fun main () = return <xml><br />
<head><br />
<title>Subrecord Constraint Witness</title><br />
</head><br />
<body><br />
<h1>Illustracion of subrecord constraint witness</h1><br />
<p><br />
It is possible using the disjointness constraint and symmetric concatenation<br />
of Ur/Web to express subrecord constraints.<br />
</p><br />
</body><br />
</xml><br />
</pre></div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/UrUr2010-12-08T01:58:59Z<p>Karn Kallio: Added link to subrecord constraint page</p>
<hr />
<div>[http://www.impredicative.com/ur/ Project web site]<br />
<br />
=== Topics ===<br />
* [[contributing to this wiki]]<br />
* [[Ur C FFI Example|C FFI Example]]<br />
* [[Ur Performance Comparisons|Performance Comparisons]]<br />
* [[Ur FAQ|Ur FAQ]]<br />
* [http://github.com/MarcWeber/vim-addon-urweb minimal Vim support]<br />
* [[companies supporting the urweb language]]<br />
* [[Impredicativity in Ur/Web]]<br />
* [[Expressing subrecord constraints]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Impredicativity_in_Ur/WebImpredicativity in Ur/Web2010-12-04T19:50:36Z<p>Karn Kallio: A simple demonstration of impredicativity in Ur/Web</p>
<hr />
<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 Kalliohttp://www.impredicative.com/wiki/index.php/UrUr2010-12-04T19:37:43Z<p>Karn Kallio: Added link to Impredicativity page</p>
<hr />
<div>[http://www.impredicative.com/ur/ Project web site]<br />
<br />
=== Topics ===<br />
* [[contributing to this wiki]]<br />
* [[Ur C FFI Example|C FFI Example]]<br />
* [[Ur Performance Comparisons|Performance Comparisons]]<br />
* [[Ur FAQ|Ur FAQ]]<br />
* [http://github.com/MarcWeber/vim-addon-urweb minimal Vim support]<br />
* [[companies supporting the urweb language]]<br />
* [[Impredicativity in Ur/Web]]</div>Karn Kalliohttp://www.impredicative.com/wiki/index.php/Companies_supporting_the_urweb_languageCompanies supporting the urweb language2010-11-19T22:53:15Z<p>Karn Kallio: Added myself ( Karn Kallio ) to list</p>
<hr />
<div>Companies don't want lock ins. So its important for them that they don't have a single point of failure.<br />
Using PHP they know that they can get support easily. So if you do or want to support urweb soon list yourself here<br />
so that customers see that they can get support easily from various providers easily.<br />
<br />
So if you're interested in supporting urweb based applications professionally add yourself here and point your potential customers to this page.<br />
<br />
== list of companies or freelancers who are interested in supporting urweb based applications ==<br />
<br />
Marc Weber (web based applications & general programming)<br />
Im Tannhörne 4/1<br />
78052 Villingen-Schwenningen<br />
email: marco-oweber@gmx.de<br />
Germany<br />
<br />
Karn Kallio ( freelance programming ) <br />
Casa 94-51<br />
Calle Sirio Entre Av. Ártico y Av. Antártico<br />
Trigal Norte, Valencia<br />
2001 Carabobo<br />
Venezuela<br />
email: tierpluspluslists@gmail.com<br />
<br />
== validated last ==<br />
Someone should step up and contact all addresses to see that they are still valid every couple of month.<br />
If you did so paste the last date here.</div>Karn Kallio