Mailing List Archive: 49091 messages
  • Home
  • Script library
  • AltME Archive
  • Mailing list
  • Articles Index
  • Site search
 

A prototype typechecker

 [1/17] 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

 [2/17] from: greggirwin:mindspring at: 7-Nov-2002 11:48


Hi Jan, Deep stuff! Given my current lack of free time and other commitments, I probably won't be able to provide any useful feedback, but I appreciate the time and effort you're contributing! I think this could be applied at the dialect level to great effect in certain cases. --Gregg

 [3/17] from: jan:skibinski:sympatico:ca at: 7-Nov-2002 18:03


Hi Gregg,
> Deep stuff! Given my current lack of free time and other commitments, I > probably won't be able to provide any useful feedback, but I appreciate the > time and effort you're contributing! >
Thanks!
> I think this could be applied at the dialect level to great effect in > certain cases.
Not that I plan to do it, at least not for quite a while, but consider this: Rebol with all its nice internet gadgetry, great flexibility and power could be used as good GUI and internet platform for other languages, such as Haskell. Despite a lot of effort, Haskell is not well equipped for this sort of things. It has only one native declarative GUI, called Fudgets, but it is a massive stuff and not in popular use. But very interesting since in priciple you *do not do* your buttons, or *do not do* your actions, but only declare how those "things" or actions could have happened if the program was to run. And when a program specification is run those things somehow magically happen. Clear as a mud? :-) Well, the thing is that Fudgets are still declarative pieces of code - they are referentially transparent, and therefore a Haskell compiler can reorganize and optimize the code any way it pleases - without introduction of side effects. So that's why Fudgets is such a big beast. On the other insteresting side, there is quite a good progress being made in Domain Specific Embedded Languages, and their practical applications in Haskell. Haskore (the program to write "symphonies" - well, almost), Fran Reactive Animation and Reactive Robotics are quite interesting projects in their own. In the meantime the main GUI effort is to interface Haskell to third party libraries: Gnome, Da Vinci, Clean's Object Library, etc. All of this require taking good care about interfacing to foreign languages. Foreign Function Interface (FFI) has been already defined but implemented mostly to interface C. This has been quite an effort, since Haskell has such a rich type system, while C or C++ are quite primitive by comparison. It's like trying to translate from PDF to text and back, if you know what I mean. :-) So if I ever consider interconnecting Haskell and Rebol, I'd better have clear idea what I am entitled to do. Obviously, the simplest approach would be to base everything on (string -> string) operations. Haskell would consider it dirty anyway and would treat them as (IO string -> IO string) types, meaning that it would try to defend itself from "pollution" by putting everything in monadic IO envelopes, whose contents could only be passed to other "dirty" monads. Anyway, this is one of my motivations for my current effort. Another one relates to documentation of complex functions, especially HOFs. I think, clearly specified patterns would tell the user in precise terms how to use such functions. I am a great believer in good documentation, and so far I was most impressed with only one language in this respect - the Eiffel. The main point here is, aside from the Design by Contract, that there is never any discrepancy between source code and documentation, because the documentation is always produced on the fly. Rebol has similar attitude and that pleases me. No stupid markup tags and all that nonsense introduced by Sun to Java. So I hope I can to contribute to this side of Rebol. The final motivation for my effort here is learning. Hands on something of significant size helps me much in discovery of mysteries of Rebol. :-) All the best, Jan

 [4/17] from: greggirwin:mindspring at: 8-Nov-2002 10:07


Hi Jan, I'm thinking of things on the user side. For us, it's a little annoying to get a "syntax error", but that kind of thing is totally foreign to normal human beings. When creating dialects, we need to take into account not only how we handle well formed input, but how we handle malformed input. The more information we gather during the parse process, the better feedback we can provide if something isn't right. Since the whole idea of a dialect is to speak *their* language - whoever "they" might be - I like the idea of dialected datatypes (for lack of a better made up term :), which is kind of what the signature and typeset view gives us. --Gregg

 [5/17] from: jan:skibinski:sympatico:ca at: 8-Nov-2002 12:57


Ooops! I meant <<grateful>>

 [6/17] from: jan:skibinski:sympatico:ca at: 8-Nov-2002 12:42


Hi Gregg,
> I'm thinking of things on the user side. For us, it's a little annoying to > get a "syntax error", but that kind of thing is totally foreign to normal
<<quoted lines omitted: 5>>
> "dialected datatypes" (for lack of a better made up term :), which is kind > of what the signature and typeset view gives us.
Thank you for this feedback. It is certainly fruitful for me. I know very little about dialects yet, except for a few I came across when browsing rebolforces articles and some WWR sites. Btw, browsing the sites from desktop is real pain - it takes too long to filter out meaningful sites from the rest. I am talking from a perspective of a newcomer, who is still unfamiliar with names of Rebolites. But if I recall there was some discussion about improvements in that area. I would be quite greatful if someone could list some useful dialects for me to peruse. Am I right to assume that Rebol 'dialects mean exactly the same as what others call DSELs - Domain Specific Embedded Languages? Jan

 [7/17] from: greggirwin:mindspring at: 8-Nov-2002 12:16


Hi Jan, JS> I would be quite greatful if someone could list some useful JS> dialects for me to peruse. Unfortunately, there aren't too many out there. Mine are very simple for the most part, and still targeted at programmers, not users. I have Logo (very simple) and AWK dialects, plus simple FSM and MAKE dialects. Mail me directly if you're interested in any of those. JS> Am I right to assume that Rebol 'dialects mean exactly JS> the same as what others call DSELs - Domain Specific Embedded JS> Languages? Yes. --Gregg

 [8/17] from: maarten:koopmans:surfnet:nl at: 8-Nov-2002 21:06


Hi Jan, Impressive, it shows once more that Rebol morphs in what you want it to be. The current Rebol type system and the way evaluation is done is causing that ;-) The fun thing is that you can change all this to help us program better, while not needing to force use of it. Unless you write your own do function, but I guess that would be a dialect. Keep up the good work! --Maarten Tue, 5 Nov 2002, Jan Skibinski wrote:

 [9/17] from: jan:skibinski:sympatico:ca at: 8-Nov-2002 17:06


Hi Maarten,
> Impressive, it shows once more that Rebol morphs in what you want it to > be. The current Rebol type system and the way evaluation is done is > causing that ;-) > > The fun thing is that you can change all this to help us program better, > while not needing to force use of it.
Very good of you to noticing it. I was almost ready to post some sort of a disclaimer, but I can see now that it is not necessery. Thanks, Jan

 [10/17] from: brett:codeconscious at: 9-Nov-2002 11:30


> JS> Am I right to assume that Rebol 'dialects mean exactly > JS> the same as what others call DSELs - Domain Specific Embedded > JS> Languages? > > Yes.
I experienced an ecclectic mixture of thoughts when reading this: 1) Guessing what others mean is always fraught :^) 2) "Domain Specific Embedded Language" doesn't sound like a useful description in the context of the goals of REBOL. "Dialect" by contrast involves human communication or at least human/computer interaction where Domain Specific Embedded Language has no such immediate meaning. Of course, I just impliedly excluded programming from human/computer interaction then, but I can do that because programmers are back to being ignored in this post IT bust :^) My real point though is that "Dialect" implies a different audience to Domain Specific Embedded Language (DSEL). I went searching using Google on "Domain Specific Embedded Language" to see what others mean by that. I found this quote "A DSEL is just a subroutine library, but written in a functional language such as Haskell." (*) Well to me that certainly doesn't sound like a good description of a dialect. I'm not entirely sure it is an accurate description of a domain specific embedded language either - but I'm not sure. Paul Hudak wrote: "... let's inherit the infrastructure of some other language---tailoring it in special ways to the domain of interest---thus yielding a domain-specific embedded language (DSEL)." (**) To me, in the context of REBOL, that last quote can provide useful understanding. But I still wonder. I agree with the last quote in general, that is REBOL dialects by definition inherit infrastructure (loaded datatypes) from their host language. But REBOL dialects do not inherit a grammar, the Dialect designer creates that. I wonder when "others" refer to DSELs in their language of interest - do they assume the grammar of the host language - perhaps even not concsiously? Maybe that is what the fellow in the first quote did.
>From the overview of "Expressions" in the REBOL core user guide:
Expressions can be processed in one of two ways: directly by the REBOL interpreter, or indirectly by a REBOL script. A script processed indirectly is called a dialect. A little further on in the user guide: "The distinction REBOL makes is that information is either directly or indirectly interpreted. The distinction is not whether information is code or data, but how it is processed." To me these descriptions invoke a broader sense of possibilities than the term DSEL does. In lines up with my believe that meaning is not *in* a message it is overlayed on a message when that message is interpreted, another reason I'm keen on REBOL. As a bit of a side note, I believe you can substitute "script" for "block" in that first user guide quote and conclude that any function that takes a block as an argument could in some sense be an interpreter of a dialect. So after all that I'd tend to a concisely answer the original questions with Probably Not - not exactly. Regards, Brett. Online references: (*) http://web.comlab.ox.ac.uk/oucl/research/areas/progtools/festabstracts/kevin .pdf (**) http://cs-www.cs.yale.edu/homes/hudak-paul/hudak-dir/ACM-WS/position.html

 [11/17] from: jan:skibinski:sympatico:ca at: 8-Nov-2002 21:18


Hi Brett, Firstly, about the online references you cited: 1-st does does not work 2-nd (Hudak's paper) seems to me quite obsolete, from 1996. Paul Hudak wrote a newer paper which expands on the one you cite by adding better introduction where clear distinction is made between DSL and DSEL and by adding some new good examples from FRAN (Functional Reactive Animation). See Hudak's paper in postscript on the FROB site (Functional Robotics) - Haskell for Vision and Robotics: http://haskell.org/frob/ Frob itself is a prime example of DSEL. The best description of DSEL used to be on Galois Connections web site. But they redesign their site every three months or so and I cannot found the references to DSELs anymore. But they do DSELs while building cryptographic software for NSA. A Haskell shop. You can find a short tutorial on FRAN here: http://www.haskell.org/fran/fran.html [Pointers to Fran at Microsoft Research do not work any more. I do not know why.] Another prime example of DSEL in Haskell is Hawk, a library for: Specifying, Verifying, and Simulating Microprocessors http://www.cse.ogi.edu/PacSoft/projects/Hawk/ There are few good presentations and tutorial there. I once prepared my own live tutorial on Hawk (to execute simulated circuits as you read) and if you really, really want to see it just ask - I can dig out the copy from the Wayback Machine. In essence: DSEL uses facilities (language features and tools) of a host language, such as Haskell, to design a DSL such as Frob. That's why I asked whether DSEL = dialect. I guess it is true but I still know too little about Rebol's dialects to be sure of that. Jan Brett Handley wrote:

 [12/17] from: brett:codeconscious at: 9-Nov-2002 13:58


Hi Jan, Thanks for the links. I wasn't trying to give an acedemic paper on the subject, just my reaction to the point that I feel there is a subtle variance in intention between the concepts.
> That's why I asked whether DSEL = dialect. I guess it is > true but I still know too little about Rebol's dialects > to be sure of that.
I take it you mean that you have used DSEL's in the past and your interest motivates you to check if that interest is supported by REBOL. I'm glad REBOL is so amenable to each of our own purposes, so that we can explore our own concepts and directions. Such a breath of fresh air. Brett.

 [13/17] from: g:santilli:tiscalinet:it at: 9-Nov-2002 11:50


Hi Jan, On Saturday, November 9, 2002, 3:18:48 AM, you wrote: JS> In essence: DSEL uses facilities (language features JS> and tools) of a host language, such as Haskell, to design JS> a DSL such as Frob. A dialect uses REBOL values to build a language. So, probably the concept is very close to that of DSEL. The only difference I can see is that REBOL's function interpreter is a dialect of the REBOL labguage, too, with "the REBOL language" being just "the REBOL values". P.S.: Jan, you might be interested in my dialect to create PDF files, aka the PDF Maker. Let me know if you want me to send a copy to you. Regards, Gabriele. -- Gabriele Santilli <[g--santilli--tiscalinet--it]> -- REBOL Programmer Amigan -- AGI L'Aquila -- REB: http://web.tiscali.it/rebol/index.r

 [14/17] from: jan:skibinski:sympatico:ca at: 9-Nov-2002 8:51


Gabriele,
> A dialect uses REBOL values to build a language. So, probably the > concept is very close to that of DSEL. The only difference I can
<<quoted lines omitted: 4>>
> files, aka the PDF Maker. Let me know if you want me to send a > copy to you.
I get local copies of all the scripts from reboltech.com/library/scripts so if your dialect PDF Maker is in the file pdf-maker.r then I already have it. But if that assumption is not correct, or your newest version has not been posted to library yet, or you have some extra documentation then yes - I would like you to send me a copy, please. Jan

 [15/17] from: g:santilli:tiscalinet:it at: 9-Nov-2002 16:46


Hi Jan, On Saturday, November 9, 2002, 2:51:04 PM, you wrote: JS> so if your dialect PDF Maker is in the file pdf-maker.r then I JS> already JS> have it. If that's the one from the library, it is probably very outdated... JS> been posted to library yet, or you have some extra documentation JS> then yes - I would like you to send me a copy, please. Some bit of documentation exists... it's not enough but is a start. You can find it on the Rebol.it REB site. Or, I will send it to you directly. Regards, Gabriele. -- Gabriele Santilli <[g--santilli--tiscalinet--it]> -- REBOL Programmer Amigan -- AGI L'Aquila -- REB: http://web.tiscali.it/rebol/index.r

 [16/17] from: jan:skibinski:sympatico:ca at: 9-Nov-2002 11:17


Hi Gabriele,
> Some bit of documentation exists... it's not enough but is a > start. You can find it on the Rebol.it REB site. Or, I will send > it to you directly.
If you don't mind please send me everything related to your pdf maker, just to be sure that I have not missed something of importance. Thanks, Jan

 [17/17] from: jan:skibinski:sympatico:ca at: 13-Nov-2002 23:22


Hi all, I'd like to update you on my progress on prototype type checker. Things go fine so far and I am testing it quite extensively using the HOF module, which I just posted to the library. I hope you will find it useful. The type checker itself uses some of the obvious patterns from the HOF script. There are still few design decisions I have to consider, such as representation for cartesian types, or for (non-rebolian) tuples. In addition to the 'check function I described before, the type checker is now directly used by a function 'chain (for lack of a better name), which provides for automatic generation of type checked partial applications; i.e., functions that take incomplete (or complete for constant functions) sets of arguments. A little sweetener shown here, the 'summary function produces summary public functions of any script - not necessary of my own. The output quality depends on how much extra information a script is able provide. summary: func [ file [file! url!] /local script names x ][ script: load/header file names: sort map :to-word sort filter :set-word? script do file print rejoin replicate 60 #"-" print rejoin ["SUMMARY of script " uppercase second split-path file] print rejoin replicate 60 #"-" foreach name names [ x: :name if any-function? get :name [ print rejoin [padd-to 20 to-string x " " mold pattern :x] ] ] ] And here is its output for HOF script: ------------------------------------------------------------ SUMMARY of script HOF.R ------------------------------------------------------------ .. ([ord] -+ [ord]) all' ((a -+ logic) -+ [a] -+ logic) and' ([logic] -+ logic) any' ((a -+ logic) -+ [a] -+ logic) cat ([[a]] -+ [a]) cycle (integer -+ [a] -+ [a]) drop (integer -+ [a] -+ [a]) drop-while ((a -+ logic) -+ [a] -+ [a]) elem (series -+ any-type -+ logic) ensure ([[logic]] -+ logic) filter ((a -+ logic) -+ [a] -+ [a]) foldl ((a -+ b -+ a) -+ a -+ [b] -+ a) foldl1 ((a -+ a -+ a) -+ [a] -+ a) foldr ((a -+ b -+ b) -+ b -+ [a] -+ b) implies (logic -+ logic -+ logic) insert-by ((a -+ a -+ logic) -+ a -+ [a] -+ [a]) iterate (integer -+ (a -+ a) -+ a -+ [a]) map ((a -+ b) -+ [a] -+ [b]) max-block ([ord] -+ ord) min-block ([ord] -+ ord) or' ([logic] -+ logic) partition ((a -+ logic) -+ [a] -+ [[a] [a]]) poly ([number] -+ number -+ number) remove-by ((a -+ a -+ logic) -+ a -+ [a] -+ [a]) replicate (integer -+ a -+ [a]) require ([[logic]] -+ logic) scanl ((a -+ b -+ a) -+ a -+ [b] -+ [a]) span ((a -+ logic) -+ [a] -+ [[a] [a]]) take (integer -+ [a] -+ [a]) take-while ((a -+ logic) -+ [a] -+ [a]) unzip ([[c]] -+ [[a] [b]]) zip ([a] -+ [b] -+ [[a b]]) Regards, Jan

Notes
  • Quoted lines have been omitted from some messages.
    View the message alone to see the lines that have been omitted