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:

    “How is freedom measured, in individuals as in nations? By the resistance which has to be overcome, by the effort it costs to stay aloft. One would have to seek the highest type of free man where the greatest resistance is constantly being overcome: five steps from tyranny, near the threshold of the danger of servitude.”
    —Friedrich Nietzsche (1844–1900)