## [REBOL] A prototype typechecker

### From: jan:skibinski:sympatico:ca at: 5-Nov-2002 23:00

Hi all, I've been working very hard in the past week or so on my prototype of a typechecker for Rebol. Since I do not currently maintain my web site, and since I do not want to pollute the library by yet another script of mine, I decided to send this l-o-o-n-g note to the mailing list. I hope you forgive me for this. I should be ready with the prototype in a few days, but since I got really tired of all that work I'd like to describe the outline of its features and ask for some feedback. Regards, Jan A typechecking session ---------------------->> check [foldl]== (foldl | (a -+ b -+ a) -+ a -+ [b] -+ a) What's that? I am asking my prototype typechecker to check a type-correctness of the expression within the block. I am starting with a sole function 'foldl. Its functionality will be explained later. For a moment let us concentrate on the types only. The typechecker says: Function 'foldl has a type shown on the right hand side of the pipe sign. The type, or a signature of this function uses two generic type variables 'a and 'b: each corresponding to any-type!. The signature sets a usage pattern, which will become more specialized down the road. The -+ symbol pretends to be an arrow separator. There are four elements in this signature: the first three types describe the types of arguments the function 'foldl will accept, and the last type is its return type. The first type on the left represents a generic function which accepts two arguments 'a and 'b, and returns a result of type 'b. In particular, 'a and 'b can be of the same type. Let's us think of a function of such type, which could be accepted by the foldl. The :add function would do, but - to make things more interesting - I will use instead my home brewed version 'sum. Back to the typechecker:>> check [foldl :sum]== (foldl :sum | ring -+ [ring] -+ ring) What's now? The typechecker says that the stuff on the left of the pipe sign is a new function, whose type is on the right. It will accept an element of type 'ring and a series of elements of type 'ring and it will produce a 'ring. The signature of the :sum itself can be checked separately:>> check [sum]== (sum | ring -+ ring -+ ring) The 'sum has been accepted as an argument to 'foldl because its type is a subset of the generic pattern advertised by 'foldl: (a -+ b -+ a) As a result the type specialization took place and the resulting type is much simple now. But what is a 'ring? This is an alias for a set of types, each having a property of a mathematical ring: with all its standard rules. This stuff is defined in the global block 'typesets:>> typesets/ring== (number money tuple pair) Please note that the ring includes neither the 'date nor the 'time: you cannot add or multiply two dates or types together. Using the typeset names instead of their explicit values has several advantages - none of the least is the space saver. Back to the typechecker: adding next argument ...>> check [foldl :sum 0]== (foldl :sum 0 | [integer] -+ integer) Now we can see even greater specialization in action: the resulting function accepts a series of integers and produces a single integer. Finally, let us provide the last missing argument, the expected series of integers:>> check [foldl :sum 0 [1 2 3 4]]== (foldl :sum 0 [1 2 3 4] | integer) Now we can safely execute the block expression>> do [foldl :sum 0 [1 2 3 4]]== 56 and obtain a sum of [1 2 3 4]. Without any detailed explanation 'foldl is a generalized accumulator, which uses a binary operator - operating on pairs of elements: one precomputed and one taken from the series. At this point I could have taken you through few other pages to demonstrate how the typechecker detects the wrong types, how to get into debugging mode (check/debug), how to show step by step reductions (check/step), etc. - but I'll spare you the pain for now. Instead, I will shortly discuss few key design factors and proposals. ============================================ The existing Rebol's system of datatypes is not good enough to support the scheme just outlined. It needs extra support for functions. The generic any-function!, function!, etc. types are not specific enough. The typechecker needs patterns: which can be either very generic, like the 'foldl pattern, or very specific, like a 'poly pattern:>> check [poly]== (poly | [number] -+ number -+ number) (Function 'poly computes value of a polynomial for a given base: 10, 16, 0.1, whatever.} I can see two ways of doing this: 1. Provide a global repository of patterns: ------------------------------------------- A small sample follows. patterns: [ map ((a -+ b) -+ [a] -+ [b]) filter ((a -+ logic) -+ [a] -+ [a]) foldl ((a -+ b -+ a) -+ a -+ [b] -+ a) poly ([number] -+ number -+ number) foldl ((a -+ a -+ a) -+ [a] -+ a) scanl ((a -+ b -+ a) -+ a -+ [b] -+ [a]) cat ([[a]] -+ [a]) .. ([ord] -+ [ord]) odd? (ord -+ logic) even? (ord -+ logic) ] As you can see, here is a mixture of few existing standard functions and some of my own. Do note that I have given very specific patterns to 'odd? and 'even? - more specific and safer that the official Rebol definitions would imply. The typeset 'ord means a set of orderable things:>> typesets/ord== (number char date money time) A very extensive table of patterns could be produced consisting of all the patterns for all existing standard functions. 2. Embedding patterns inside the new functions ---------------------------------------------- This alternative has several advantages and disadvantages compared to the former method. I will skip their discussion for the moment but instead show a source of the 'sum function, that has been created using this method: sum: formal-function [ {A wrapper around a :+ operator to limit its usage to typeset 'ring. This example also shows one of two ways to specify formal usage 'pattern for a function. (ring -+ ring -+ ring) } x [(typeset ring)] y [(typeset ring)] /local result [(typeset ring)] ][ pattern (ring -+ ring -+ ring) ][ result: x + y result ] 3. Existing typesets can be captured and stored in the global block 'typesets ------------------------------------- The example shown here demonstrates my laziness in the name invention. A good deal of thought should be required to make it palatable. typesets: [ generic (a b c d e f) or-able (logic number char tuple binary image) add-able (number pair char money date time tuple) multiply-able (number pair char money time tuple) skip-able (series port) bind-able (block word) find-able (series port bitset) exclude-able (series bitset) difference-able (series bitset date) parse-able (block string none) save-able (file url binary) set-able (any-word block) pick-able (series pair event money date time object port tuple any-function) ord (number char date money time) ring (number money tuple pair) ] ============================================ That's it! Thank's for you attention. I will post the prototype typechecker as soon as I am comfortable with it more or less. It will override the file %signature.r Jan