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:

    “The more characteristic American hero in the earlier day, and the more beloved type at all times, was not the hustler but the whittler.”
    —Mark Sullivan (1874–1952)