From 84d60f7602acc1351a28bb02e40fa8625ee07d8a Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 7 Dec 2005 11:53:29 +0000 Subject: Transfer reference: operators, overloading --- doc/transfer-reference.html | 271 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 253 insertions(+), 18 deletions(-) (limited to 'doc/transfer-reference.html') diff --git a/doc/transfer-reference.html b/doc/transfer-reference.html index 7670da8b8..8a7fa85d7 100644 --- a/doc/transfer-reference.html +++ b/doc/transfer-reference.html @@ -7,7 +7,7 @@

Transfer language reference

Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Wed Dec 7 11:02:54 2005 +Last update: Wed Dec 7 12:50:46 2005

@@ -42,11 +42,20 @@ Last update: Wed Dec 7 11:02:54 2005
  • String literal patterns
  • Integer literal patterns -
  • Metavariables -
  • Overloaded functions / Type classes -
  • Operators -
  • Compositional functions -
  • do notation +
  • Metavariables +
  • Overloaded functions + +
  • Standard prelude +
  • Operators + +
  • Compositional functions +
  • do notation

    @@ -287,37 +296,52 @@ where exp1 must be an expression of type Bool.

    Records

    +

    Record types

    Record types are created by using a sig expression: 

    -  sig { p1 : T1; ... ; pn : Tn }
+  sig { l1 : T1; ... ; ln : Tn }

    -Here, p1 to pn are the field labels and T1 to Tn are their types. +Here, l1 to ln are the field labels and T1 to Tn are field types.

    +

    Record values

    Record values are constructed using rec expressions: 

    -  rec { p1 = exp1; ... ; pn = expn }
+  rec { l1 = exp1; ... ; ln = expn }
+
    +

    +

    Record projection

    +

    +Fields are selection from records using the . operator. This expression selects +the field l from the record value r: +

    +
    +  r.l

    +

    Records and layout syntax

    The curly braces and semicolons are simply explicit layout syntax, so the record type and record expression above can also be written as: 

    -  sig p1 : T1
-      pn : Tn
+  sig l1 : T1
+      ...
+      ln : Tn
 

    -  rec p1 = exp1
-      pn = expn
+  rec l1 = exp1
+      ...
+      ln = expn

    +

    Record subtyping

    A record of some type R1 can be used as a record of any type R2 @@ -513,7 +537,7 @@ String literals can be used as patterns.

    Integer literals can be used as patterns.

    - +

    Metavariables

    Metavariable are written as questions marks: @@ -523,7 +547,7 @@ Metavariable are written as questions marks:

    -A metavariable is a way to the the Transfer type checker that: +A metavariable is a way to the the type checker that: "you should be able to figure out what this should be, I can't be bothered to tell you".

    @@ -532,12 +556,223 @@ Metavariables can be used to avoid having to give type and dictionary arguments explicitly.

    -

    Overloaded functions / Type classes

    +

    Overloaded functions

    +

    +In Transfer, functions can be overloaded by having them take a record +of functions as an argument. For example, the functions for equality +and inequality in the Transfer prelude module are defined as: +

    +
    +  Eq : Type -> Type
+  Eq A = sig eq : A -> A -> Bool
+  
+  eq : (A : Type) -> Eq A -> A -> A -> Bool
+  eq _ d = d.eq
+  
+  neq : (A : Type) -> Eq A -> A -> A -> Bool
+  neq A d x y = not (eq A d x y)
+
    +

    +

    +We call Eq a type class, though it's actually just a record type +used to pass function implementations to overloaded functions. We +call a value of type Eq A an Eq dictionary for the type A. +The dictionary is used to look up the version of the function for the +particular type we want to use the function on. Thus, in order to use +the eq function on two integers, we need a dictionary of type +Eq Integer: +

    +
    +  eq_Integer : Eq Integer
+  eq_Integer = rec eq = prim_eq_Integer
+
    +

    +

    +where prim_eq_Integer is the built-in equality function for +integers. To check whether two numbers x and y are equal, we +can then call the overloaded eq function with the dictionary: +

    +
    +  eq Integer eq_Integer x y
+
    +

    +

    +Giving the type at which to use the overloaded function, and the appropriate +dictionary is cumbersome. Metavariables come to the rescue: +

    +
    +  eq ? ? x y
+
    +

    +

    +The type checker can in most cases figure out the values of the type and +dictionary arguments. NOTE: this is not implemented yet. +

    -

    Operators

    +

    Type class extension

    +

    +By using record subtyping, see Record subtyping, we can +create type classes which extend other type classes. A dictionary for the +new type class can also be used as a dictionary for old type class. +

    +

    +For example, we can extend the Eq type class above to Ord, a type +class for orderings: +

    +
    +  Ord : Type -> Type
+  Ord A = sig eq : A -> A -> Bool
+              compare : A -> A -> Ordering
+
    +

    +

    +To extend an existing class, we keep the fields of the class we want to +extend, and add any new fields that we want. Because of record subtyping, +for any type A, a value of type Ord A is also a value of type Eq A. +

    -

    Compositional functions

    +

    Extending multiple classes

    +

    +A type class can also extend several classes, by simply having all the fields +from all the classes we want to extend. The Num class described below is +an example of this. +

    +

    Standard prelude

    +

    +The standard prelude, see prelude.tra +contains definitions of a number of standard types, functions and +type classes. +

    + +

    Operators

    + +

    Unary operators

    + + + + + + + + + + + +
    OperatorPrecedenceTranslation
    -10-x => negate ? ? x
    + +

    + +

    Binary operators

    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    OperatorPrecedenceAssociativityTranslation of x op y
    >>=3leftbind ? ? x y
    >>3leftbind ? ? x (\_ -> y)
    ||4rightif x then True else y
    &&5rightif x then y else False
    ==6noneeq ? ? x y
    /=6noneneq ? ? x y
    <6nonelt ? ? x y
    <=6nonele ? ? x y
    >6nonegt ? ? x y
    >=6nonege ? ? x y
    ::7rightCons ? ? x y
    +8leftplus ? ? x y
    -8leftminus ? ? x y
    *9lefttimes ? ? x y
    /9leftdiv ? ? x y
    %9leftmod ? ? x y
    + +

    + +

    Compositional functions

    +

    do notation

    Sequences of operations in the Monad type class can be written -- cgit v1.2.3