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:

    “There is a limit to the application of democratic methods. You can inquire of all the passengers as to what type of car they like to ride in, but it is impossible to question them as to whether to apply the brakes when the train is at full speed and accident threatens.”
    —Leon Trotsky (1879–1940)