For some time, rather desultorily recently, I'll admit, I've been
working on Qi/tk. But when complete it will amount to a complete type
secure GUI builder with all the GUI power of TCL/tk and a user-
programmable interface and connection to the web. This is part of the
L21 project (http://www.lambdassociates.org/lC21.htm).
It's significant work and rather hard to develop, requiring detailed
knowledge of TCL/tk and command of Qi's sequent notation and how it
works. To give you an idea of just how complex just the type theory
is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
size of Qi itself! Without Qi technology I really couldn't hope to
attempt this task.
My original intention had been to release it, like Qi, as a complete
system in its own right. But Qi took years and I don't want to repeat
a Sisyphean task. Hence Qi/tk has sat on my machine for a long time.
So what I've decided to do is to develop this system through a series
of phased releases in which a block at a time is released, tested
under the open source community at Qilang, corrected and improved
through your feedback.
If you're a Qi/Lisp programmer you are very welcome to contribute to
this project which will be run at Qilang and the sources placed in
the
open source Qi repository run by J.T. Gleason. The index page at
www.lambdassociates.org will give you the current state of Qi/tk and
how to help.
Here are the planned phases; being released at a rate of at least one
a week until block 5. Initially we will be working in Windows CLisp
only. By the release of the last block we should have the realised
the
goals of phase 3 of L21.
Tell me what you think!
Qi/tk 1.0E Block 1
________________
1.0E means 'experimental version 1.0'.
Components:
Foreign language Interface;
- opening a channel to a foreign program via a stream
- open-process-stream : string --> [string] --> stream
- 5 basic functions for communicating with other languages
and their types
- talk : (string --> stream --> [A])
- listen : (number --> stream --> string)
- talk-and-listen : (string --> number --> stream --> string)
- listen-and-act : (number --> stream --> unit)
- talk-listen-and-act : (string --> number --> stream --> unit)
Operating System Interface
- sending commands to the OS and receiving the response
Documentation
Comments: this is low level stuff *written in Lisp* with a wrapper of
type theory. It's important in providing a simple way for newbies to
get Qi to talk to other applications. The later blocks all run off
this. Good Lisp programmers can help here.
Status: implemented.
Qi/tk 1.0E Block 2
_____________________
Components:
Synchronous Qi/tk top level
Documentation
Comments: this is a top level that allows you to run the GUI
synchronously with the read-evaluate-print loop. In other words you
do not have to put your program into an event loop to interact with
your GUI. Carl Shapiro and I wrote some of this code in 2004.
This is again written in Lisp.
Status: implemented
Qi/tk 1.0E Block 3
_____________________
Components:
Buttons
Window Manager
Property List Attribute Model of Widgets
Comments: this will provide high-level code for creating buttons and
introduce the window manager commands. All widget properties will be
held when possible in Lisp property lists and will be accessible
through type secure commands. Likewise the 30+ attributes of buttons
will be given a type theory.
This is written in Lisp and Qi.
Status: largely implemented.
Qi/tk 1.0E Block 4
_____________________
Components:
Labels
Reading web pages
Type Theory
Documentation
Comments: this will provide high-level code for creating labels.
This is written in Lisp and Qi.
Status: largely implemented.
Qi/tk 1.0E Block 5
_____________________
Components:
Images
Colours
Fonts
Type Theory
Documentation
Comments: none needed.
This is written in Lisp and Qi.
Status: largely implemented.
Qi/tk 1.0E Block 6
___________________
Components:
Entries
Textboxes
Type Theory
Documentation
Comments: none
Status: largely implemented
Qi/tk 1.0E Block 7
___________________
Components:
Dialog Windows
Winfo function
Type Theory
Documentation
Comments: the latter has a complex type theory
Status: largely implemented
Qi/tk 1.0E Block 8
___________________
Components:
radiobuttons
checkbuttons
Type Theory
Documentation
Comments: none
Status: largely implemented
Qi/tk 1.0E Block 9
___________________
Components:
menus
Type Theory
Documentation
Comments: the most complex widget in Tk.
Status: unimplemented
Qi/tk 1.0E Block 10
___________________
Components:
defining widgets through type secure inheritance
user defined attributes of widgets
constraint handling, dynamically linking slot values
Status: unimplemented
Feedback welcome.
Mark
From: Matthias Buelow
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <5gfdssF3g89f3U1@mid.dfncis.de>
Mark Tarver wrote:
> It's significant work and rather hard to develop, requiring detailed
> knowledge of TCL/tk and command of Qi's sequent notation and how it
> works. To give you an idea of just how complex just the type theory
> is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
> size of Qi itself! Without Qi technology I really couldn't hope to
> attempt this task.
I think you're approaching this from the wrong direction...
Mark Tarver wrote:
> For some time, rather desultorily recently, I'll admit, I've been
> working on Qi/tk. But when complete it will amount to a complete type
> secure GUI builder with all the GUI power of TCL/tk and a user-
> programmable interface and connection to the web. This is part of the
> L21 project (http://www.lambdassociates.org/lC21.htm).
>
> It's significant work and rather hard to develop, requiring detailed
> knowledge of TCL/tk and command of Qi's sequent notation and how it
> works. To give you an idea of just how complex just the type theory
> is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
> size of Qi itself! Without Qi technology I really couldn't hope to
> attempt this task.
You may be interested in the LablTK bindings to Tk in the OCaml standard
library, which provide Tk interoperability with the assurances of static
typing. They weigh in at 41kLOC of OCaml, which is ~9% of the OCaml
distribution.
There are also 74kLOC of bindings to GTK2 as a separate package: LablGTK2.
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
> You may be interested in the LablTK bindings to Tk in the OCaml standard
> library, which provide Tk interoperability with the assurances of static
> typing.
Right; seems sensisble.
< They weigh in at 41kLOC of OCaml, which is ~9% of the OCaml
> distribution.
>
> There are also 74kLOC of bindings to GTK2 as a separate package: LablGTK2.
>
> --
> Dr Jon D Harrop, Flying Frog Consultancy
> OCaml for Scientistshttp://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
Yes; 41k LOC does not surprise me. The saving grace is that my 12k
LOC are machine-generated from Qi and are not hand written. The hand
written sources are only 1.5k LOC of largely sequent calculus.
Mark
Mark Tarver wrote:
> Yes; 41k LOC does not surprise me. The saving grace is that my 12k
> LOC are machine-generated from Qi and are not hand written. The hand
> written sources are only 1.5k LOC of largely sequent calculus.
That's very nice. If I were to write such libraries, I would use a similar
approach. However, if you want to provide a sane and native-friendly
representation of the underlying API there is going to be a lot of work
that (probably) cannot be automated.
I'm looking forward to using the autogenerated GLCaml bindings to OpenGL
2.1:
http://glcaml.sourceforge.net/
In the case of an evolving API such as OpenGL, I think it is essential to
automate as much of the low-level interface code generation as possible,
just as you have done.
I have long thought that bindings to good libraries are a real weak point of
all functional programming languages, so it is always good to see better
libraries being created and released. I wonder if there is any scope for
collaboration between the major FPL communities in trying to improve this
situation...
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
From: Daniel Trstenjak
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <20070722140719.GA7205@linux.ver>
On Sun, Jul 22, 2007 at 08:44:41AM +0100, Jon Harrop wrote:
> I have long thought that bindings to good libraries are a real weak point of
> all functional programming languages, so it is always good to see better
> libraries being created and released. I wonder if there is any scope for
> collaboration between the major FPL communities in trying to improve this
> situation...
Are you thinking about an abstract definition of bindings in a
functional style, which could be the source for the automatically
generation of language specific bindings?
Regards,
Daniel
Daniel Trstenjak wrote:
> On Sun, Jul 22, 2007 at 08:44:41AM +0100, Jon Harrop wrote:
>> I have long thought that bindings to good libraries are a real weak point
>> of all functional programming languages, so it is always good to see
>> better libraries being created and released. I wonder if there is any
>> scope for collaboration between the major FPL communities in trying to
>> improve this situation...
>
> Are you thinking about an abstract definition of bindings in a
> functional style, which could be the source for the automatically
> generation of language specific bindings?
I was thinking more along the lines of a higher-level intermediate API that
provided static typing and run-time types. That way dynamically typed
languages can ignore the static types and statically typed languages can
progagate them.
This is not too dissimilar to .NET and interoperating with C# from F# is
vastly nicer than interoperating with (say) C++ from OCaml.
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
From: Matthias Buelow
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <5ghgf3F3gslhmU1@mid.dfncis.de>
Jon Harrop wrote:
> I was thinking more along the lines of a higher-level intermediate API that
> provided static typing and run-time types. That way dynamically typed
> languages can ignore the static types and statically typed languages can
> progagate them.
It would make a lot more sense (imho) to have it the other way round, if
restricted (statically typed) languages sit on top of a dynamic library.
It won't make any difference to the restricted language but won't
restrict dynamic languages binding against the library. In a concrete
example, it would make sense, imho, to have Lisp and Lisp libraries as
the basis, and build restricted languages such as ML etc. as special
purpose cases on top of this system.
Matthias Buelow wrote:
> Jon Harrop wrote:
>> I was thinking more along the lines of a higher-level intermediate API
>> that provided static typing and run-time types. That way dynamically
>> typed languages can ignore the static types and statically typed
>> languages can progagate them.
>
> It would make a lot more sense (imho) to have it the other way round, if
> restricted (statically typed) languages sit on top of a dynamic library...
That's what I was suggesting, yes. The next question is: for what definition
of "type"? I suppose it should be the intersection of Haskell/OCaml/Lisp as
these are the three biggest FPLs. I think that gives us:
Int : int
Float : float
Char : char
String : char array
Array : obj array | 'a array
List : obj list | 'a list
Function : obj -> obj | 'a -> 'b
So dynamic languages can treat everything as being derived from obj and
static languages can distinguish between types and enforce correctness.
> In a concrete example, it would make sense, imho, to have Lisp and Lisp
> libraries as the basis...
Yes. It would need more than this to be useful though: the API would need to
be static-type friendly and the implementation would need to provide
machine-verifiable static type information for a common type system.
Now that I look at it, this has all been done before in the context of RPCs
and web services. Perhaps a better solution would be to expose useful APIs
in that form rather than reinventing the wheel here, i.e. put an RPC
interface on GTK.
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
From: Joachim Durchholz
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <f81nr6$lkq$2@online.de>
Matthias Buelow schrieb:
> Jon Harrop wrote:
>
>> I was thinking more along the lines of a higher-level intermediate API that
>> provided static typing and run-time types. That way dynamically typed
>> languages can ignore the static types and statically typed languages can
>> progagate them.
>
> It would make a lot more sense (imho) to have it the other way round, if
> restricted (statically typed) languages sit on top of a dynamic library.
> It won't make any difference to the restricted language but won't
> restrict dynamic languages binding against the library. In a concrete
> example, it would make sense, imho, to have Lisp and Lisp libraries as
> the basis, and build restricted languages such as ML etc. as special
> purpose cases on top of this system.
The statically-typed languages would be unable to take advantage of the
static typing present in the library that way, and always have trouble
finding an efficient way to use such a library.
Regards,
Jo
From: Ken Tilton
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <tHJoi.16$OB6.11@newsfe12.lga>
Jon Harrop wrote:
> Mark Tarver wrote:
>
>>For some time, rather desultorily recently, I'll admit, I've been
>>working on Qi/tk. But when complete it will amount to a complete type
>>secure GUI builder with all the GUI power of TCL/tk and a user-
>>programmable interface and connection to the web. This is part of the
>>L21 project (http://www.lambdassociates.org/lC21.htm).
>>
>>It's significant work and rather hard to develop, requiring detailed
>>knowledge of TCL/tk and command of Qi's sequent notation and how it
>>works. To give you an idea of just how complex just the type theory
>>is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
>>size of Qi itself! Without Qi technology I really couldn't hope to
>>attempt this task.
>
>
> You may be interested in the LablTK bindings to Tk in the OCaml standard
> library, which provide Tk interoperability with the assurances of static
> typing. They weigh in at 41kLOC of OCaml, which is ~9% of the OCaml
> distribution.
>
> There are also 74kLOC of bindings to GTK2 as a separate package: LablGTK2.
>
My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
task. Or was it Sisyphean? Some Egyptiam, anyway.
Have we identified a problem with Qi/OCaml?
kt
On 22 Jul, 15:20, Ken Tilton <···········@optonline.net> wrote:
> Jon Harrop wrote:
> > Mark Tarver wrote:
>
> >>For some time, rather desultorily recently, I'll admit, I've been
> >>working on Qi/tk. But when complete it will amount to a complete type
> >>secure GUI builder with all the GUI power of TCL/tk and a user-
> >>programmable interface and connection to the web. This is part of the
> >>L21 project (http://www.lambdassociates.org/lC21.htm).
>
> >>It's significant work and rather hard to develop, requiring detailed
> >>knowledge of TCL/tk and command of Qi's sequent notation and how it
> >>works. To give you an idea of just how complex just the type theory
> >>is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
> >>size of Qi itself! Without Qi technology I really couldn't hope to
> >>attempt this task.
>
> > You may be interested in the LablTK bindings to Tk in the OCaml standard
> > library, which provide Tk interoperability with the assurances of static
> > typing. They weigh in at 41kLOC of OCaml, which is ~9% of the OCaml
> > distribution.
>
> > There are also 74kLOC of bindings to GTK2 as a separate package: LablGTK2.
>
> My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
> week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
> task. Or was it Sisyphean? Some Egyptiam, anyway.
>
> Have we identified a problem with Qi/OCaml?
>
> kt- Hide quoted text -
>
> - Show quoted text -
Well I can't speak for Jon; though on past record I'm sure silence
will not be an option ;).
The 12,000 lines is actually machine generated code from 800 lines of
sequent calculus. You get a big blow up. This in Qi sequent
calculus
X : A; Y : B;
_____________
(@p X Y) : (A * B);
becomes this in Lisp
(PROG2 (INCF *logical-inferences*)
(LET ((X915 (lazyderef FP1)))
(AND (CONSP X915)
(LET ((X916 (lazyderef (CAR X915))))
(AND (EQ X916 ·@p)
(LET ((X917 (lazyderef (CDR X915))))
(AND (CONSP X917)
(LET ((X (CAR X917)))
(LET ((X918 (lazyderef (CDR X917))))
(AND (CONSP X918)
(LET ((Y (CAR X918)))
(LET ((X919 (lazyderef (CDR X918))))
(AND (EQ X919 NIL)
(LET ((X920 (lazyderef FP2)))
(IF (CONSP X920)
(LET ((A (CAR X920)))
(LET ((X921 (lazyderef (CDR X920))))
(AND (CONSP X921)
(LET ((X922 (lazyderef (CAR X921))))
(AND (EQ X922 '*)
(LET ((X923 (lazyderef (CDR X921))))
(AND (CONSP X923)
(LET ((B (CAR X923)))
(LET ((X924 (lazyderef (CDR X923))))
(AND (EQ X924 NIL)
(tt* X A FP3
#'(LAMBDA NIL
(tt* Y B FP3
Continuation)))))))))))))
(AND (var? X920)
(LET ((A (GENSYM "V")) (B (GENSYM "V")))
(PROGV (LIST X920) (LIST (CONS A (CONS '* (CONS B
NIL))))
(tt* X A FP3
#'(LAMBDA NIL
(tt* Y B FP3
Continuation)))))))))))))))))))))
There's about 2,000 lines of Qi/Lisp needed plus about 100 pages of
documentation plus several shake-down implementations which right now
is a lot in relation to my available resources which are very thin at
the moment, but improving. Its harder - not necessarily longer in Qi
- than writing the untyped version in Lisp because you have to think
about more things.
If the OCaml people wrote > 40k lines then maybe they had to hand-
write the code I am generating. I can believe that a complete type
theory for TCL/tk might be that long. But Jon will no doubt enlighten
us.
Mark
Mark Tarver wrote:
> If the OCaml people wrote > 40k lines then maybe they had to hand-
> write the code I am generating. I can believe that a complete type
> theory for TCL/tk might be that long. But Jon will no doubt enlighten
> us.
I had actually made two mistakes:
1. I counted all of the code in the OCaml tool stack and examples using Tk
rather than just the bindings, which are only 10kLOC.
2. Some of it is indeed autogenerated, though I'm not exactly what.
In the case of the GTK bindings, there is 12kLOC of (presumably)
hand-written source and another 5kLOC autogenerated.
Might be interesting to see what Haskell offers as well...
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
Mark Tarver wrote:
> If the OCaml people wrote > 40k lines then maybe they had to hand-
> write the code I am generating. I can believe that a complete type
> theory for TCL/tk might be that long. But Jon will no doubt enlighten
> us.
I had actually made two mistakes:
1. I counted all of the code in the OCaml tool stack and examples using Tk
rather than just the bindings, which are only 10kLOC.
2. Some of it is indeed autogenerated, though I'm not exactly what.
In the case of the GTK bindings, there is 12kLOC of (presumably)
hand-written source and another 5kLOC autogenerated.
Might be interesting to see what Haskell offers as well...
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
Ken Tilton wrote:
> My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
> week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
> task. Or was it Sisyphean? Some Egyptiam, anyway.
>
> Have we identified a problem with Qi/OCaml?
Probably need to compare features to find out. What programs are written
using Cells-Gtk, how much of GTK (2?) does it support, is it safe etc.?
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
From: Ken Tilton
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <ATLoi.33$OB6.12@newsfe12.lga>
Jon Harrop wrote:
> Ken Tilton wrote:
>
>>My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
>>week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
>>task. Or was it Sisyphean? Some Egyptiam, anyway.
>>
>>Have we identified a problem with Qi/OCaml?
>
>
> Probably need to compare features to find out. What programs are written
> using Cells-Gtk, how much of GTK (2?) does it support, is it safe etc.?
>
The Cells-Gtk list is relatively active, seems to be in danger of
picking up new committers cuz they have been offering stuff. GTK2, yes.
"How much", don't know, but a lot of macrology hides all the boilerplate
that goes into gluing things, so a whole new module just means a couple
dozen lines of CL -- we sure ain't gonna catch Qi/Ocaml at that rate.
"Safe"? That begs the question: yes, we understand the "safe" /claim/
for typefussy languages. My question is, Is this what happens when you
try to use them for real-word tasks such as absorbing a foreign language
GUI library? Later we can debate whether the claim stands up in the face
of making programming so hard that Qi has punted on Tk bindings.
Forget the LOC question, why is it /hard/? I would give Cells the
credit, but Celtk actually started with LTk as a platform.
kenzo
--
http://www.theoryyalgebra.com/
"Algebra is the metaphysics of arithmetic." - John Ray
"As long as algebra is taught in school,
there will be prayer in school." - Cokie Roberts
"Stand firm in your refusal to remain conscious during algebra."
- Fran Lebowitz
"I'm an algebra liar. I figure two good lies make a positive."
- Tim Allen
On 22 Jul, 17:50, Ken Tilton <···········@optonline.net> wrote:
> Jon Harrop wrote:
> > Ken Tilton wrote:
>
> >>My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
> >>week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
> >>task. Or was it Sisyphean? Some Egyptiam, anyway.
>
> >>Have we identified a problem with Qi/OCaml?
>
> > Probably need to compare features to find out. What programs are written
> > using Cells-Gtk, how much of GTK (2?) does it support, is it safe etc.?
>
> The Cells-Gtk list is relatively active, seems to be in danger of
> picking up new committers cuz they have been offering stuff. GTK2, yes.
> "How much", don't know, but a lot of macrology hides all the boilerplate
> that goes into gluing things, so a whole new module just means a couple
> dozen lines of CL -- we sure ain't gonna catch Qi/Ocaml at that rate.
>
> "Safe"? That begs the question: yes, we understand the "safe" /claim/
> for typefussy languages. My question is, Is this what happens when you
> try to use them for real-word tasks such as absorbing a foreign language
> GUI library? Later we can debate whether the claim stands up in the face
> of making programming so hard that Qi has punted on Tk bindings.
>
> Forget the LOC question, why is it /hard/? I would give Cells the
> credit, but Celtk actually started with LTk as a platform.
>
> kenzo
>
> --http://www.theoryyalgebra.com/
>
> "Algebra is the metaphysics of arithmetic." - John Ray
>
> "As long as algebra is taught in school,
> there will be prayer in school." - Cokie Roberts
>
> "Stand firm in your refusal to remain conscious during algebra."
> - Fran Lebowitz
>
> "I'm an algebra liar. I figure two good lies make a positive."
> - Tim Allen
I'm not certain why you think that something you've never done is
easy. Try for example, thinking about the type of the winfo command
in TCL/tk. It does have a type theory but its not manifest; you have
to extract it.
> Forget the LOC question, why is it /hard/? I would give Cells the
> credit, but Celtk actually started with LTk as a platform.
You've answered your own question at the bottom of your post.
> I would give Cells the
> credit, but Celtk actually started with LTk as a platform.
> "Safe"? That begs the question: yes, we understand the "safe" /claim/
> for typefussy languages. My question is, Is this what happens when you
> try to use them for real-word tasks
A lot of your current work would benefit greatly from looking at some
of the techniques I've been experimenting with. See the study on
algebra in www.lambdassociates.org.* Types and pattern-oriented
programming would shorten your algebra program and increase its
reliability. Seriously.
This is the largest most complex type theory Qi has encoded; so if it
can handle it, its a real proof of the viability of my approach. Now
I've got to do what I set out to do.
Mark
* http://www.lambdassociates.org/studies/study07.htm
From: Ken Tilton
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <cqSoi.354$fy4.54@newsfe12.lga>
Mark Tarver wrote:
> On 22 Jul, 17:50, Ken Tilton <···········@optonline.net> wrote:
>
>>Jon Harrop wrote:
>>
>>>Ken Tilton wrote:
>>
>>>>My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
>>>>week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
>>>>task. Or was it Sisyphean? Some Egyptiam, anyway.
>>
>>>>Have we identified a problem with Qi/OCaml?
>>
>>>Probably need to compare features to find out. What programs are written
>>>using Cells-Gtk, how much of GTK (2?) does it support, is it safe etc.?
>>
>>The Cells-Gtk list is relatively active, seems to be in danger of
>>picking up new committers cuz they have been offering stuff. GTK2, yes.
>>"How much", don't know, but a lot of macrology hides all the boilerplate
>>that goes into gluing things, so a whole new module just means a couple
>>dozen lines of CL -- we sure ain't gonna catch Qi/Ocaml at that rate.
>>
>>"Safe"? That begs the question: yes, we understand the "safe" /claim/
>>for typefussy languages. My question is, Is this what happens when you
>>try to use them for real-word tasks such as absorbing a foreign language
>>GUI library? Later we can debate whether the claim stands up in the face
>>of making programming so hard that Qi has punted on Tk bindings.
>>
>>Forget the LOC question, why is it /hard/? I would give Cells the
>>credit, but Celtk actually started with LTk as a platform.
>>
...
> I'm not certain why you think that something you've never done is
> easy.
You might be taking me too literally, always a clever way of ducking a
point. The point is....
> Try for example, thinking about the type of the winfo command
> in TCL/tk. It does have a type theory but its not manifest; you have
> to extract it.
Fine. So merely sorting out the type system of an /existing library/ is
so insanely hard that Qi does not have TK bindings, and advocates of
statically typed languages want developers likewise wrestling with type
theory at the same time as they are developing their applications, when
the type theory is constantly shifting because, in reality, the type
"theory" is derivative from what the developer wants to do with their
data. Static languages put the type theory cart before the horse,
breaking the development process. Yummy.
>
>
>>Forget the LOC question, why is it /hard/? I would give Cells the
>>credit, but Celtk actually started with LTk as a platform.
>
>
> You've answered your own question at the bottom of your post.
>
>
>>I would give Cells the
>>credit, but Celtk actually started with LTk as a platform.
>
>
>>"Safe"? That begs the question: yes, we understand the "safe" /claim/
>>for typefussy languages. My question is, Is this what happens when you
>>try to use them for real-word tasks
>
>
> A lot of your current work would benefit greatly from looking at some
> of the techniques I've been experimenting with. See the study on
> algebra in www.lambdassociates.org.* Types and pattern-oriented
> programming would shorten your algebra program and increase its
> reliability. Seriously.
Seriously, it would seem you gave no idea wherein lies the hard part of
developing serious educational Algebra software. It certainly has
nothing to do with the Algebra.
>
> This is the largest most complex type theory Qi has encoded; so if it
> can handle it, its a real proof of the viability of my approach. Now
> I've got to do what I set out to do.
Best of luck, anyway.
ken
Jon Harrop <···@ffconsultancy.com> writes:
> Ken Tilton wrote:
> > My Celtk project comes in at 6k, Cells-Gtk at 10k. Qi makes what was one
> > week's effort (Celtk, followed by Vasily's Cells-Gtk) into a Herculean
> > task. Or was it Sisyphean? Some Egyptiam, anyway.
> >
> > Have we identified a problem with Qi/OCaml?
>
> Probably need to compare features to find out. What programs are written
> using Cells-Gtk, how much of GTK (2?) does it support, is it safe etc.?
I don't know if it's safe. But you certainly don't have to worry about
something like this happening:
# let rec f n = if n <= 1 then 1 else n * f (n-1);;
val f : int -> int = <fun>
# f 42;;
- : int = -1685313281113194496
Yes, I know about BigInt. And I'm sure you know about ASSERT.
Andras
Andras Simon wrote:
> # let rec f n = if n <= 1 then 1 else n * f (n-1);;
> val f : int -> int = <fun>
> # f 42;;
> - : int = -1685313281113194496
>
> Yes, I know about BigInt. And I'm sure you know about ASSERT.
True. Does GTK use big ints throughout then? ;-)
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
On Jul 21, 10:40 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> For some time, rather desultorily recently, I'll admit, I've been
> working on Qi/tk. But when complete it will amount to a complete type
> secure GUI builder with all the GUI power of TCL/tk and a user-
> programmable interface and connection to the web. This is part of the
> L21 project (http://www.lambdassociates.org/lC21.htm).
>
> It's significant work and rather hard to develop, requiring detailed
> knowledge of TCL/tk and command of Qi's sequent notation and how it
> works. To give you an idea of just how complex just the type theory
> is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
> size of Qi itself! Without Qi technology I really couldn't hope to
> attempt this task.
You should not be proud of this, you should not be posting this in
public: you should be ashamed, and you should be searching for a
language that gives you some benefit and productivity!
Ltk is not perfect, nor perfectly complete, but it's industrial
quality for single-threaded, multi-threaded, and serve-event back-
ends; it comes with demos and error handlers for interactive
development and production use; and all that in well *UNDER* 2k LOC
(according to read/print/"wc -l" with a *print-right-margin* of 100).
The last bits of Tk coverage and object verification which stand
between here and Ltk 1.0 will *maybe* bloat that count from 1.8x k to
1.9k. Maybe.
And to to denigrate Peter Herth, but I don't think he counts Ltk as a
great scientific achievement, but rather as a great hack. If you're
proud of your achievement in getting Tk bindings for your language,
you should be ashamed of your language.
"Thomas F. Burdick" <········@gmail.com> writes:
>
>> It's significant work and rather hard to develop, requiring detailed
>> knowledge of TCL/tk and command of Qi's sequent notation and how it
>> works. To give you an idea of just how complex just the type theory
>> is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
>> size of Qi itself! Without Qi technology I really couldn't hope to
>> attempt this task.
>
> You should not be proud of this, you should not be posting this in
> public: you should be ashamed, and you should be searching for a
> language that gives you some benefit and productivity!
Elsewhere he notes that it's only something like 800 lines of Qi code,
which get turned into 12,000 lines elsewhere. That's actually a good
example of using a language to make things easier, I'd think...
--
Robert Uhl <http://public.xdi.org/=ruhl>
Considering the number of wheels Microsoft has found reason to invent,
one never ceases to be baffled by the minuscule number whose shape
even vaguely resembles a circle. --unknown
Robert Uhl <·········@NOSPAMgmail.com> writes:
> Elsewhere he notes that it's only something like 800 lines of Qi code,
> which get turned into 12,000 lines elsewhere. That's actually a good
> example of using a language to make things easier, I'd think...
I think it's also indicative that tcl/tk is an awful hack.
Paul Rubin wrote:
> Robert Uhl <·········@NOSPAMgmail.com> writes:
>
>>Elsewhere he notes that it's only something like 800 lines of Qi code,
>>which get turned into 12,000 lines elsewhere. That's actually a good
>>example of using a language to make things easier, I'd think...
>
>
> I think it's also indicative that tcl/tk is an awful hack.
Might be another slam on Qi/OCaml: I certainly had to work around things
in Tk I thought could have been handled better, but nothing close to a
show-stopper. Overall it is a great platform for a language like CL.
Even gets us some libs for free.
kt
--
http://www.theoryyalgebra.com/
"Algebra is the metaphysics of arithmetic." - John Ray
"As long as algebra is taught in school,
there will be prayer in school." - Cokie Roberts
"Stand firm in your refusal to remain conscious during algebra."
- Fran Lebowitz
"I'm an algebra liar. I figure two good lies make a positive."
- Tim Allen
> Paul Rubin wrote:
>> Robert Uhl <·········@NOSPAMgmail.com> writes:
>>
>>>Elsewhere he notes that it's only something like 800 lines of Qi code,
>>>which get turned into 12,000 lines elsewhere. That's actually a good
>>>example of using a language to make things easier, I'd think...
>> I think it's also indicative that tcl/tk is an awful hack.
>
> Might be another slam on Qi/OCaml: I certainly had to work around
> things in Tk I thought could have been handled better, but nothing
> close to a show-stopper. Overall it is a great platform for a language
> like CL. Even gets us some libs for free.
And why might that be "another slam on ... Ocaml"? Am I missing
something deep and profound in this thread?
Regards -- Markus
From: Ken Tilton
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <Fa6pi.12$3Q4.9@newsfe12.lga>
Markus E Leypold wrote:
>>Paul Rubin wrote:
>>
>>>Robert Uhl <·········@NOSPAMgmail.com> writes:
>>>
>>>
>>>>Elsewhere he notes that it's only something like 800 lines of Qi code,
>>>>which get turned into 12,000 lines elsewhere. That's actually a good
>>>>example of using a language to make things easier, I'd think...
>>>
>>>I think it's also indicative that tcl/tk is an awful hack.
>>
>>Might be another slam on Qi/OCaml: I certainly had to work around
>>things in Tk I thought could have been handled better, but nothing
>>close to a show-stopper. Overall it is a great platform for a language
>>like CL. Even gets us some libs for free.
>
>
> And why might that be "another slam on ... Ocaml"? Am I missing
> something deep and profound in this thread?
Yes, but as with many IRs yours is too terse to determine exactly what.
It's like getting to the end of Moby Dick and asking, "What whale?".
kxo
> Markus E Leypold wrote:
>>>Paul Rubin wrote:
>>>
>>>>Robert Uhl <·········@NOSPAMgmail.com> writes:
>>>>
>>>>
>>>>>Elsewhere he notes that it's only something like 800 lines of Qi code,
>>>>>which get turned into 12,000 lines elsewhere. That's actually a good
>>>>>example of using a language to make things easier, I'd think...
>>>>
>>>>I think it's also indicative that tcl/tk is an awful hack.
>>>
>>>Might be another slam on Qi/OCaml: I certainly had to work around
>>>things in Tk I thought could have been handled better, but nothing
>>>close to a show-stopper. Overall it is a great platform for a language
>>>like CL. Even gets us some libs for free.
>> And why might that be "another slam on ... Ocaml"? Am I missing
>> something deep and profound in this thread?
>
> Yes, but as with many IRs yours is too terse to determine exactly
> what. It's like getting to the end of Moby Dick and asking, "What
> whale?".
Thanks. That answer, though superficially about something completely
unrelated (Moby, Dick, whales, the undefined identifier 'IR' whose
meaning I cannot determine from context: Here 'Isoprene Rubber' makes
as much sense as 'Infrared Radiation') carries a subtext message
that is exactly to the point: You passed the troll test. Not
surprising indeed, after your rant against strong static type systems
(somehwere earlier in this tangle of threads) I was almost convinced
already, but it's good to get affirmation.
Regards -- Markus
PS: For your information where your camouflage systems failed: OCaml
has zilch to do with Qi and no problem with integrating Tk.
Markus E Leypold wrote:
> And why might that be "another slam on ... Ocaml"? Am I missing
> something deep and profound in this thread?
You've not missed anything.
--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?usenet
From: Ken Tilton
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <h07pi.21$271.3@newsfe12.lga>
Jon Harrop wrote:
> Markus E Leypold wrote:
>
>>And why might that be "another slam on ... Ocaml"? Am I missing
>>something deep and profound in this thread?
>
>
> You've not missed anything.
>
It is funny how quiet you get when you have no answer. Static typing
RIP, get over it.
kenny
From: Matthias Buelow
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <5gkd0rF3g5gvvU1@mid.dfncis.de>
Ken Tilton wrote:
> It is funny how quiet you get when you have no answer. Static typing
> RIP, get over it.
Gladly you take on where he leaves off...
> Jon Harrop wrote:
>> Markus E Leypold wrote:
>>
>>>And why might that be "another slam on ... Ocaml"? Am I missing
>>>something deep and profound in this thread?
>> You've not missed anything.
>>
>
> It is funny how quiet you get when you have no answer. Static typing
> RIP, get over it.
Indeed there is nothing we need to say. You already got enough rope
...
Just to help you to start your act: What you wrote, so far, were
representations of your beliefs. They are certainly deeply felt, but
at our side there is some difficulty to comprehend and appraise them
to their full glorious extent. Since you seem to be very convinced of
your point of view (I hope not without reason), but haven't brought
forward any substantiating arguments so far, would you kindly do us
the favour to elaborate your theories and deduce suppositions from
premises more commonly accepted as valid or probable either in the
industry or in academia. Don't spare us references to literature or
text books if you don't mind.
(and now please get into your rope act: I'm already thrilled).
Regards -- Markus
Robert Uhl wrote:
> "Thomas F. Burdick" <········@gmail.com> writes:
>
>>>It's significant work and rather hard to develop, requiring detailed
>>>knowledge of TCL/tk and command of Qi's sequent notation and how it
>>>works. To give you an idea of just how complex just the type theory
>>>is - it scales in at 12,000 lines of Lisp and rising. That is 2X the
>>>size of Qi itself! Without Qi technology I really couldn't hope to
>>>attempt this task.
>>
>>You should not be proud of this, you should not be posting this in
>>public: you should be ashamed, and you should be searching for a
>>language that gives you some benefit and productivity!
>
>
> Elsewhere he notes that it's only something like 800 lines of Qi code,
> which get turned into 12,000 lines elsewhere. That's actually a good
> example of using a language to make things easier, I'd think...
>
I think you missed the bit where he said the work is hard. You (aided
and abetted) have fixated on LOC. "Hard" is not in the LOC, it is in the
analysis of the type theory implicit in Tk.
kt
From: Joachim Durchholz
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <f84qr3$cvv$1@online.de>
Ken Tilton schrieb:
> I think you missed the bit where he said the work is hard. You (aided
> and abetted) have fixated on LOC. "Hard" is not in the LOC, it is in the
> analysis of the type theory implicit in Tk.
That's more an argument against Tk than against static typing.
A good, straightforward GUI library has a simple type theory.
"Complicated type theory" means "gratuitously complicated semantics",
with awkwardness like having to parse outputs or checking that a given
field exists, instead of simply picking up the interesting details from
a simple data structure. (Having to parse and check field existence also
tends to be more fragile across a library's evolution than having a
solid type structure, however informal, which means that the assumptions
that your client code relies on may be changed behind your back.)
Complicated types are OK during design space exploration, but not when
the code goes into real use. Not for libraries anyway, where even a
tenfold design effort that gives just a meager 10% easier use would help
10,000s of programmers.
Regards,
Jo
On 23 Jul, 00:06, "Thomas F. Burdick" <········@gmail.com> wrote:
> On Jul 21, 10:40 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>
> > For some time, rather desultorily recently, I'll admit, I've been
> > working on Qi/tk. But when complete it will amount to a complete type
> You should not be proud of this, you should not be posting this in
> public: you should be ashamed,
I personally am not interested in adding complex type theory on top of
a GUI toolkit written in a language where everything's a string. But
I'm happy to be educated by one of the Dr's as to why this is a good
thing.
On the other hand, the cleverness in binding to TK isn't just getting
it working. I can (and have) spawned wish as a subprocess, added
controls and handled callbacks to Lisp in around 20 lines of code. But
it's not comfortable to program like this as you're just shunting Tcl
strings to a sub-process. The nice thing about LTK, as you know, is
that it provides a great deal of programmer comfort in the form of a
CLOS based widget abstraction.
--
Phil
http://phil.nullable.eu/
···············@gmail.com writes:
> On 23 Jul, 00:06, "Thomas F. Burdick" <········@gmail.com> wrote:
> > On Jul 21, 10:40 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
> >
> > > For some time, rather desultorily recently, I'll admit, I've been
> > > working on Qi/tk. But when complete it will amount to a complete type
>
> > You should not be proud of this, you should not be posting this in
> > public: you should be ashamed,
>
> I personally am not interested in adding complex type theory on top of
> a GUI toolkit written in a language where everything's a string.
It clearly isn't _useful_, that's for sure.
> But I'm happy to be educated by one of the Dr's as to why this is a
> good thing.
I'm guessing that for MT it would be a "good thing" in the academic
sense that sequent type theory can maybe handle something like this.
Shrug. Of course, as alluded to, it's not clear how one could ever be
sure you actually achieved this since the "type theory" in tk isn't
manifest (only "implicit") and thus whatever you come up with may well
be incorrect, insufficient, or otherwise inadequate.
/Jon
--
'j' - a n t h o n y at romeo/charley/november com
P� Tue, 24 Jul 2007 18:15:23 +0200, skrev jayessay <······@foo.com>:
> ···············@gmail.com writes:
>
>> On 23 Jul, 00:06, "Thomas F. Burdick" <········@gmail.com> wrote:
>> > On Jul 21, 10:40 pm, Mark Tarver <··········@ukonline.co.uk> wrote:
>> >
>> > > For some time, rather desultorily recently, I'll admit, I've been
>> > > working on Qi/tk. But when complete it will amount to a complete
>> type
>>
>> > You should not be proud of this, you should not be posting this in
>> > public: you should be ashamed,
>>
>> I personally am not interested in adding complex type theory on top of
>> a GUI toolkit written in a language where everything's a string.
>
> It clearly isn't _useful_, that's for sure.
>
>
>> But I'm happy to be educated by one of the Dr's as to why this is a
>> good thing.
>
The failure is using tcl/tk under the hood.
Use JNI with a SWING interface or .NET and types make perfect sense.
Personally I have always avoided Tk because it requires me to use
a Tcl interpreter. I used PythonTk when I programmed Python and found it a
fast and convenient library for simple apps. However it got complex the
more you
needed to customize the default behaviour. Also since Tcl is slow
performance suffers
when you need lot's of custom code.
--
Sendt med Operas revolusjonerende e-postprogram: http://www.opera.com/mail/
From: Joachim Durchholz
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <f84r4o$da7$1@online.de>
···············@gmail.com schrieb:
>
> I personally am not interested in adding complex type theory on top of
> a GUI toolkit written in a language where everything's a string.
The complex type theory is already in it, it's just not explicitly
written down.
Having a complete type theory of an interface means having all relevant
preconditions and postconditions for every of its functions.
Regards,
Jo
> ···············@gmail.com schrieb:
>>
>> I personally am not interested in adding complex type theory on top of
>> a GUI toolkit written in a language where everything's a string.
>
> The complex type theory is already in it, it's just not explicitly
> written down.
The question, of course, is, wether it is compatible with the type
theory of a given language and wether a union of both "aligns well"
with constructing a GUI in a modular way. Sometimes I
doubt. E.g. building a GUI with typed fields (you can only input
numbers in number fields, subranges in the corresponding in fields
with subrange types etc) and handling input in a typesafe way from GUI
to application core and back again (including the problem of temporary
invalid input like "2.1.4" or "214" in a subrange field with max_entry
= 30.0 which occurs almost naturally if one needs to move a decimal
point) -- all this seems to be really difficult even with a type
system with parametric polymorphism. My experience is that one
duplicates knowledge about the invariants in the application core and
in teh GUI making the result difficult to maintain.
But YMMV.
> Having a complete type theory of an interface means having all relevant
> preconditions and postconditions for every of its functions.
I doubt you can map all pre- and postconditions to one of the existing
type systems (though I agree, typed GUIs would be rather desirable).
Regards -- Markus
From: Joachim Durchholz
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <f87cj1$7tb$1@online.de>
Markus E Leypold schrieb:
>> Having a complete type theory of an interface means having all relevant
>> preconditions and postconditions for every of its functions.
>
> I doubt you can map all pre- and postconditions to one of the existing
> type systems (though I agree, typed GUIs would be rather desirable).
The type system would have to be somewhere between Hindley-Milner and a
fully Turing-Complete one, i.e. it would most likely be undecidable.
Which means we're not going to get such a type system in production
quality anytime soon.
(The other problem is that few of the type theorists have more than a
vague idea how an average programmer could work with such a type system.
So even when a good type theory is found, it will take a few years until
it has been massages into something that average and below-average
programmers can find useful.)
Regards,
Jo
On 25 Jul, 12:36, Joachim Durchholz <····@durchholz.org> wrote:
> (The other problem is that few of the type theorists have more than a
> vague idea how an average programmer could work with such a type system.
> So even when a good type theory is found, it will take a few years until
> it has been massages into something that average and below-average
> programmers can find useful.)
I guess that makes me an "average programmer". I like to write
software that people use rather than papers that nobody reads.
--
Phil
http://phil.nullable.eu/
> Markus E Leypold schrieb:
>>> Having a complete type theory of an interface means having all
>>> relevant preconditions and postconditions for every of its
>>> functions.
>> I doubt you can map all pre- and postconditions to one of the
>> existing
>> type systems (though I agree, typed GUIs would be rather desirable).
>
> The type system would have to be somewhere between Hindley-Milner and
> a fully Turing-Complete one, i.e. it would most likely be undecidable.
>
> Which means we're not going to get such a type system in production
> quality anytime soon.
Or never: AFAIK "undecidable" means undecidable in principle, not just
"we don't happen to know the right algorithm". Indeed I think that
type systems and proofs on pre- and post-conditions should be
seperated: Type system decide the representation on the underlying
host and ensure that execution is always well defined (no "undefined"
behaviour). All the pre- and post-condition stuff should be a separate
system which probably would be entangled with something like a proof
assistant in the compiler. An advantage would be that proofing would
not have to happen at any compiler run (well typed programs always
have well defined behaviour), but just when the programmer decides
she/he wants an optimized program version (information from pre and
post-condiations could be used to optimize the program) or she/he
wants actually to proof that the program is adhering to the specs.
> (The other problem is that few of the type theorists have more than a
> vague idea how an average programmer could work with such a type
> system. So even when a good type theory is found, it will take a few
> years until it has been massages into something that average and
> below-average programmers can find useful.)
So probably not in our lifetime. A pity, actually. But on the other
side, in a world still dominated by C/C++ a "real" type system (as HM)
already brings huge advantages in comparison: Catches most of the
usual errors / typos, and parametric polymorphism mitigates the
(percieved) necessity to circumvent the type system. So HM already
gives one, I'd say 90% or more of what is urgently needed. The
pressure to develop more comprehensive (type or proof) system is
correspondingly low. (And that again is perhaps a good idea
considering how premature adoption of a concept or idea by the
industry can cripple it (the concept or idea) for years because poorly
understood implemementations will be put out and become religion,
augmented by more magic and superstition if salvation does not come as
expected).
Regards -- Markus
From: Joachim Durchholz
Subject: Re: Releasing Qi/tk - a new model of development
Date:
Message-ID: <f87kq3$hpa$1@online.de>
Markus E Leypold schrieb:
>> Markus E Leypold schrieb:
>>>> Having a complete type theory of an interface means having all
>>>> relevant preconditions and postconditions for every of its
>>>> functions.
>>> I doubt you can map all pre- and postconditions to one of the
>>> existing
>>> type systems (though I agree, typed GUIs would be rather desirable).
>> The type system would have to be somewhere between Hindley-Milner and
>> a fully Turing-Complete one, i.e. it would most likely be undecidable.
>>
>> Which means we're not going to get such a type system in production
>> quality anytime soon.
>
> Or never: AFAIK "undecidable" means undecidable in principle, not just
> "we don't happen to know the right algorithm".
Undecidability doesn't mean the problem is intractable in practice.
The usual shortcut here is that a human is asked for hints that will
help the program complete its task. This is what most proof systems do
anyway.
> Indeed I think that
> type systems and proofs on pre- and post-conditions should be
> seperated: Type system decide the representation on the underlying
> host and ensure that execution is always well defined (no "undefined"
> behaviour). All the pre- and post-condition stuff should be a separate
> system which probably would be entangled with something like a proof
> assistant in the compiler.
The type of the values that might be bound of the name can be normal
pre- or postconditions.
If you have a proof assistant in the compiler, it should be smart enough
to do type inference.
The assertions should be differentiated between "must be proven at
compile time" and "I can live with run-time checking", not between "this
is type-related" and "this is value-related".
IMHO.
Regards,
Jo