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