Qi (programming Language) - Type Checking

Type Checking

Static typing is optional in Qi and is enabled by (tc +) and disabled by (tc -). The type system recognises symbols, variables, strings, booleans, numbers and characters as primitive types. Primitive type operators are list, * (product), --> and array. Here are some examples

(3-) (tc +) true (4+) hello hello : symbol (5+) "hello" "hello" : string (6+) 686.8 686.8 : number (7+) #\z #\z : character (8+) true true : boolean (9+) (@p 1 a) (@p 1 a) : (number * symbol) (10+) ] : (list number) (11+) (* 8) # : (number --> number) (12+) X X : variable

Functions are explicitly typed as with Hope. is an acceptable abbreviation for the type (list A). Here is the polytype signature of member in Qi.

(define member {A --> --> boolean} _ -> false X -> true X -> (member X Y))

User-defined concrete types are defined in Qi sequent calculus. Qi sequent calculus uses a single conclusion formalism. Sequent rules have the form

S1; . . . Sn; ____ S0;

where S0,...,Sn are sequent patterns. Note that S1, ...,Sn may be empty.

Side conditions in Qi are either (a) boolean tests or (b) local assignments. Here are some examples; the first uses a boolean side-condition to define an enumeration type 'fruit' containing 'apples', 'pears' and 'oranges' as the only inhabitants.

(7+)(datatype fruit if (element? F ) ______________________________________ F : fruit;) fruit : unit (8+) apples : fruit apples : fruit (9+) plums : fruit error: type error

Here a type 'alphanum' is defined that is the union of the types of symbols and numbers.

(10+) (datatype alphanum X : number; ___________ X : alphanum; X : symbol; ___________ X : alphanum;) alphanum : unit (11+) : (list alphanum)

Here is a (rather fatuous) use of local assignments in a type.

(12+) (datatype ordering if (number? X) if (number? Y) let Z (* X 2) if (= Y Z) __________________ : ordering;) ordering : unit (13+) : ordering error: type failure (14+) : ordering : ordering

Lastly a more interesting recursive type for binary numbers.

(15+) (datatype binary if (element? X ) _____________ X : zero-or-one; X : zero-or-one; __________________ : binary; X : zero-or-one; Y : binary; ____________________________ : binary; X : zero-or-one, : binary >> P; ___________________________________________ : binary >> P;) binary (16+) (define complement \calculates the complement of a binary number\ {binary --> binary} -> -> -> )] -> )]) complement : (binary --> binary) (3+) (complement ) : binary

Read more about this topic:  Qi (programming Language)

Famous quotes containing the word type:

    ““... In truth I find it ridiculous that a man of his intelligence suffer over this type of person, who is not even interesting, for she is said to be foolish”, she added with all the wisdom of people who are not in love, who find that a sensible man should only be unhappy over a person who is worthwhile; it is almost tantamount to being surprised that anyone deign having cholera for having been infected with a creature as small as the vibrio bacilla.”
    —Marcel Proust (1871–1922)