Cat version 0.7
Christopher Diggins — 2006-09-29 06:04:20
There has been a new version of Cat released into the public domain at
http://www.cat-language.com . This version introduces a lot of bug
fixes, and is undergoing more rigorous testing.
The core functionality of Cat is now all present, I just need to
reintroduce all of the atomic operations (which are dormant in the
code) and do a ton more testing before I can officially declare a 1.0
definitely by Christmas.
Try out the type inference engine, it is neat-o!
- Christopher
Robbert van Dalen — 2006-09-29 21:44:58
Hi Christopher,
I've just downloaded your source code. I can't execute
the executable or compile the source but I can see
where you're heading to: everything looks nice and
firm.
My question to you is: why are you so focused on
types? Is that because of the Forth legacy - wrong
types and crash - or that Joy isn't particularly
focused on the notion of types?
Another question to you is: why does Cat allow mutable
constructs? I know your beautiful type system can
catch the difference between clean and dirty stuff
(which is great) but why even allow such impure things
to penetrate Cat?
Nevertheless, it's good to see that you and me (being
absolute newcomers) are eager to carry the vision of
Manfred von Thun to the future - not forgetting Slava
Pestov with his Factor language of course.
I think we should listen carefully to what the
concatenative list has to say about Cat, Enchilada or
Factor - the records say they haven't been doing much
else for the past 15 years ;)
You've got my vote.
Cheers,
Robbert.
--- Christopher Diggins <
cdiggins@...> wrote:
> There has been a new version of Cat released into
> the public domain at
> http://www.cat-language.com . This version
> introduces a lot of bug
> fixes, and is undergoing more rigorous testing.
>
> The core functionality of Cat is now all present, I
> just need to
> reintroduce all of the atomic operations (which are
> dormant in the
> code) and do a ton more testing before I can
> officially declare a 1.0
> definitely by Christmas.
>
> Try out the type inference engine, it is neat-o!
>
> - Christopher
>
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Christopher Diggins — 2006-09-30 04:43:00
I'm sorry that the executable and source code didn't work for you (is
it because you don't have C#, and the .NET framework installed?). I
appreciate the encouragement though.
My focus on types is motivated by the fact that for non-trivial
software (100,000 lines and plus) they become extremely important for
catching errors early in the development process. Typeless languages
simply don't scale well for large projects.
There aren't any mutable constructs in Cat. The notion of purity
models whether a function has a dependency on an external state
I hope this answers your questions?
Thanks again for your feedback and support,
Christopher Diggins
On 9/29/06, Robbert van Dalen <r_v_dalen@...> wrote:
>
>
>
>
>
>
> Hi Christopher,
>
> I've just downloaded your source code. I can't execute
> the executable or compile the source but I can see
> where you're heading to: everything looks nice and
> firm.
>
> My question to you is: why are you so focused on
> types? Is that because of the Forth legacy - wrong
> types and crash - or that Joy isn't particularly
> focused on the notion of types?
>
> Another question to you is: why does Cat allow mutable
> constructs? I know your beautiful type system can
> catch the difference between clean and dirty stuff
> (which is great) but why even allow such impure things
> to penetrate Cat?
>
> Nevertheless, it's good to see that you and me (being
> absolute newcomers) are eager to carry the vision of
> Manfred von Thun to the future - not forgetting Slava
> Pestov with his Factor language of course.
>
> I think we should listen carefully to what the
> concatenative list has to say about Cat, Enchilada or
> Factor - the records say they haven't been doing much
> else for the past 15 years ;)
>
> You've got my vote.
>
> Cheers,
> Robbert.
>
>
> --- Christopher Diggins <cdiggins@...> wrote:
>
> > There has been a new version of Cat released into
> > the public domain at
> > http://www.cat-language.com . This version
> > introduces a lot of bug
> > fixes, and is undergoing more rigorous testing.
> >
> > The core functionality of Cat is now all present, I
> > just need to
> > reintroduce all of the atomic operations (which are
> > dormant in the
> > code) and do a ton more testing before I can
> > officially declare a 1.0
> > definitely by Christmas.
> >
> > Try out the type inference engine, it is neat-o!
> >
> > - Christopher
> >
>
> __________________________________________________
> Do You Yahoo!?
> Tired of spam? Yahoo! Mail has the best spam protection around
> http://mail.yahoo.com
>
>
>
William Tanksley, Jr — 2006-09-30 04:33:16
Robbert van Dalen <
r_v_dalen@...> wrote:
> My question to you is: why are you so focused on
> types? Is that because of the Forth legacy - wrong
> types and crash - or that Joy isn't particularly
> focused on the notion of types?
I'm not him, but if I were I'd probably answer "because it's an
interesting problem." :-)
IMO typeless languages are fun and easy to work with, but typed
languages have some uses, and conceptually, types make it easier to
think about some things.
> Another question to you is: why does Cat allow mutable
> constructs? I know your beautiful type system can
> catch the difference between clean and dirty stuff
> (which is great) but why even allow such impure things
> to penetrate Cat?
What's impure about mutable data? The reality is, that's how computers work.
> I think we should listen carefully to what the
> concatenative list has to say about Cat, Enchilada or
> Factor - the records say they haven't been doing much
> else for the past 15 years ;)
Cheers to the people who actually DO something!!!!
> Robbert.
-Billy
Christopher Diggins — 2006-09-30 06:14:08
On 9/29/06, William Tanksley, Jr <
wtanksleyjr@...> wrote:
>
> Robbert van Dalen <r_v_dalen@...> wrote:
> > My question to you is: why are you so focused on
> > types? Is that because of the Forth legacy - wrong
> > types and crash - or that Joy isn't particularly
> > focused on the notion of types?
>
> I'm not him, but if I were I'd probably answer "because it's an
> interesting problem." :-)
That definitely plays into it. :-)
> IMO typeless languages are fun and easy to work with, but typed
> languages have some uses, and conceptually, types make it easier to
> think about some things.
My view on types is that it makes it easier to
1) verify that a program does what you expect
2) tell someone what it is that you think the program should do.
Number two is interesting because I could actually write a simple
type->english translator which describes the high level results of
functions.
I want to point out that typed languages, don't neccessarily require
type annotations. That is the joy of type inference (pun intended).
> > Another question to you is: why does Cat allow mutable
> > constructs? I know your beautiful type system can
> > catch the difference between clean and dirty stuff
> > (which is great) but why even allow such impure things
> > to penetrate Cat?
>
> What's impure about mutable data? The reality is, that's how computers work.
Yes I agree. I use the term "pure" to refer to whether functions are
guaranteed to return the same value given the same input from the two
stacks. Referentially transparent I think is the correct term. Impure
functions are definitely crucial to doing meaningful things with a
machine.
> > I think we should listen carefully to what the
> > concatenative list has to say about Cat, Enchilada or
> > Factor - the records say they haven't been doing much
> > else for the past 15 years ;)
>
> Cheers to the people who actually DO something!!!!
And cheers to the people who think carefully about things and discuss
them intelligently and pleasantly. :-)
> > Robbert.
Christopher
Robbert van Dalen — 2006-09-30 14:50:50
Somehow my post got lost. Hopefully it will not appear
twice.
> > I'm not him, but if I were I'd probably answer
> "because it's an
> > interesting problem." :-)
>
> That definitely plays into it. :-)
>
> > IMO typeless languages are fun and easy to work
> with, but typed
> > languages have some uses, and conceptually, types
> make it easier to
> > think about some things.
>
> My view on types is that it makes it easier to
> 1) verify that a program does what you expect
> 2) tell someone what it is that you think the
> program should do.
Yes, types can help understand programs in a
declaritive manner. But I think the most (interesting
but complex) problems are encounted at runtime.
Examples are: network timeouts, exhaustive memory
usage/swapping, infinite loops, dead-locks,
race-conditions, layered and recast exceptions, etc,
etc.
All these problems I've encountered multiple times in
Java programs (which is a strongly typed language) and
types didn't help me there. In fact, types that are
declared as one thing, but behave like another is the
worst situation you can get into.
That's why I'm moving away from OO and stateful
programs. Big OO implementations just don't scale in
practise.
> I want to point out that typed languages, don't
> neccessarily require
> type annotations. That is the joy of type inference
> (pun intended).
That's what I like more. Automatically infering the
type (or meaning) of programs. But that's more related
to theorem proving I would say.
> > > Another question to you is: why does Cat allow
> mutable
> > > constructs? I know your beautiful type system
> can
> > > catch the difference between clean and dirty
> stuff
> > > (which is great) but why even allow such impure
> things
> > > to penetrate Cat?
> >
> > What's impure about mutable data? The reality is,
> that's how computers work.
>
> Yes I agree. I use the term "pure" to refer to
> whether functions are
> guaranteed to return the same value given the same
> input from the two
> stacks. Referentially transparent I think is the
> correct term. Impure
> functions are definitely crucial to doing meaningful
> things with a
> machine.
With the current state of machines - yes. For
instance, the Intel processor is continiously
destroying information (and generating a lot of heat
doing that). See
http://en.wikipedia.org/wiki/Reversible_computing for
an alternative.
Wouldn't it be great if we can ban the destruction of
information all together, even at the hardware level?
:-)
> > > I think we should listen carefully to what the
> > > concatenative list has to say about Cat,
> Enchilada or
> > > Factor - the records say they haven't been doing
> much
> > > else for the past 15 years ;)
> >
> > Cheers to the people who actually DO something!!!!
>
> And cheers to the people who think carefully about
> things and discuss
> them intelligently and pleasantly. :-)
Hear, hear! But to rephrase my (somewhat wrongly put)
statement: what I meant to say was: we should pay
attention to what the concatenative list has/had to
say: they have been implementing, discussing and
argueing about Joy for almost a decade.
I have found myself searching the archives numerious
times when I got stuck on a certain concatenative
problem.
And always found something valuable that helped me
solve it (hitting a lot of Manfred's, Billy's and
Stevan's posts as a result).
> Christopher
>
Robbert.
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Robbert van Dalen — 2006-09-30 10:56:50
> > I'm not him, but if I were I'd probably answer
> "because it's an
> > interesting problem." :-)
>
> That definitely plays into it. :-)
>
> > IMO typeless languages are fun and easy to work
> with, but typed
> > languages have some uses, and conceptually, types
> make it easier to
> > think about some things.
>
> My view on types is that it makes it easier to
> 1) verify that a program does what you expect
> 2) tell someone what it is that you think the
> program should do.
Yes, types can help understand programs in a
declaritive manner. But I think the most (interesting
but complex) problems are encounted at runtime.
Examples are: network timeouts, exhaustive memory
usage/swapping, infinite loops, dead-locks,
race-conditions, layered and recast exceptions, etc,
etc.
All these problems I've encountered multiple times in
Java programs (which is a strongly typed language) and
types didn't help me there. In fact, types that are
declared as one thing, but behave like another is the
worst situation you can get into.
That's why I'm moving away from OO and stateful
programs. Big OO implementations just don't scale in
practise.
> I want to point out that typed languages, don't
> neccessarily require
> type annotations. That is the joy of type inference
> (pun intended).
That's what I like more. Automatically infering the
type (or meaning) of programs. But that's more related
to theorem proving I would say.
> > > Another question to you is: why does Cat allow
> mutable
> > > constructs? I know your beautiful type system
> can
> > > catch the difference between clean and dirty
> stuff
> > > (which is great) but why even allow such impure
> things
> > > to penetrate Cat?
> >
> > What's impure about mutable data? The reality is,
> that's how computers work.
>
> Yes I agree. I use the term "pure" to refer to
> whether functions are
> guaranteed to return the same value given the same
> input from the two
> stacks. Referentially transparent I think is the
> correct term. Impure
> functions are definitely crucial to doing meaningful
> things with a
> machine.
With the current state of machines - yes. For
instance, the Intel processor is continiously
destroying information (and generating a lot of heat
doing that). See
http://en.wikipedia.org/wiki/Reversible_computing for
an alternative.
Wouldn't it be great if we can ban the destruction of
information all together, even at the hardware level?
:-)
> > > I think we should listen carefully to what the
> > > concatenative list has to say about Cat,
> Enchilada or
> > > Factor - the records say they haven't been doing
> much
> > > else for the past 15 years ;)
> >
> > Cheers to the people who actually DO something!!!!
>
> And cheers to the people who think carefully about
> things and discuss
> them intelligently and pleasantly. :-)
Hear, hear! But to rephrase my (somewhat wrongly put)
statement: what I meant to say was: we should pay
attention to what the concatenative list has/had to
say: they have been implementing, discussing and
argueing about Joy for almost a decade.
I have found myself searching the archives numerious
times when I got stuck on a certain concatenative
problem.
And always found something valuable that helped me
solve it (hitting a lot of Manfred's, Billy's and
Stevan's posts as a result).
> Christopher
>
Robbert.
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
stevan apter — 2006-09-30 18:55:54
----- Original Message -----
From: "Robbert van Dalen" <r_v_dalen@...>
To: <concatenative@yahoogroups.com>
Sent: Saturday, September 30, 2006 10:50 AM
Subject: Re: [stack] Cat version 0.7
> Somehow my post got lost. Hopefully it will not appear
> twice.
in that case, anyone not persuaded by reading the first
copy could read the second.
>
> > > I'm not him, but if I were I'd probably answer
> > "because it's an
> > > interesting problem." :-)
ditto
> >
> > That definitely plays into it. :-)
> >
> > > IMO typeless languages are fun and easy to work
> > with, but typed
> > > languages have some uses, and conceptually, types
> > make it easier to
> > > think about some things.
> >
> > My view on types is that it makes it easier to
> > 1) verify that a program does what you expect
> > 2) tell someone what it is that you think the
> > program should do.
>
> Yes, types can help understand programs in a
> declaritive manner. But I think the most (interesting
> but complex) problems are encounted at runtime.
> Examples are: network timeouts, exhaustive memory
> usage/swapping, infinite loops, dead-locks,
> race-conditions, layered and recast exceptions, etc,
> etc.
this is absolutely right. combinatorial unit-testing
(the poor man's substitute for static typing) will get
you just so far. when the environment is scaled-up
in any of the dimensions you describe -- size of data,
number of processes/connections, frequency of messages,
&c. -- things get unpredictable in a hurry. i guess
i shouldn't be surprised that your summary sounds like
you've been working in the office next to mine, since
these scale-problems are, as you say, an aspect of
computing in any language, typed or not.
> All these problems I've encountered multiple times in
> Java programs (which is a strongly typed language) and
> types didn't help me there. In fact, types that are
> declared as one thing, but behave like another is the
> worst situation you can get into.
> That's why I'm moving away from OO and stateful
> programs. Big OO implementations just don't scale in
> practise.
i've believed that to be true for fifteen years. the
only way to defeat scaling phenomena is to make the
target-problem smaller (that's a k talking-point.)
> > I want to point out that typed languages, don't
> > neccessarily require
> > type annotations. That is the joy of type inference
> > (pun intended).
> That's what I like more. Automatically infering the
> type (or meaning) of programs. But that's more related
> to theorem proving I would say.
>
> > > > Another question to you is: why does Cat allow
> > mutable
> > > > constructs? I know your beautiful type system
> > can
> > > > catch the difference between clean and dirty
> > stuff
> > > > (which is great) but why even allow such impure
> > things
> > > > to penetrate Cat?
> > >
> > > What's impure about mutable data? The reality is,
> > that's how computers work.
> >
> > Yes I agree. I use the term "pure" to refer to
> > whether functions are
> > guaranteed to return the same value given the same
> > input from the two
> > stacks. Referentially transparent I think is the
> > correct term. Impure
> > functions are definitely crucial to doing meaningful
> > things with a
> > machine.
> With the current state of machines - yes. For
> instance, the Intel processor is continiously
> destroying information (and generating a lot of heat
> doing that). See
> http://en.wikipedia.org/wiki/Reversible_computing for
> an alternative.
> Wouldn't it be great if we can ban the destruction of
> information all together, even at the hardware level?
> :-)
yes.
>
> > > > I think we should listen carefully to what the
> > > > concatenative list has to say about Cat,
> > Enchilada or
> > > > Factor - the records say they haven't been doing
> > much
> > > > else for the past 15 years ;)
> > >
> > > Cheers to the people who actually DO something!!!!
> >
> > And cheers to the people who think carefully about
> > things and discuss
> > them intelligently and pleasantly. :-)
> Hear, hear! But to rephrase my (somewhat wrongly put)
> statement: what I meant to say was: we should pay
> attention to what the concatenative list has/had to
> say: they have been implementing, discussing and
> argueing about Joy for almost a decade.
> I have found myself searching the archives numerious
> times when I got stuck on a certain concatenative
> problem.
> And always found something valuable that helped me
> solve it (hitting a lot of Manfred's, Billy's and
> Stevan's posts as a result).
we're eagerly awaiting The Return of Manfred.
>
> > Christopher
> >
>
> Robbert.
>
>
> __________________________________________________
> Do You Yahoo!?
> Tired of spam? Yahoo! Mail has the best spam protection around
> http://mail.yahoo.com
>
>
>
> Yahoo! Groups Links
>
>
>
>
>
>
>
>
Greg Buchholz — 2006-09-30 18:55:50
--- Robbert van Dalen <
r_v_dalen@...> wrote:
> Yes, types can help understand programs in a
> declaritive manner. But I think the most (interesting
> but complex) problems are encounted at runtime.
> Examples are: network timeouts, exhaustive memory
> usage/swapping, infinite loops, dead-locks,
> race-conditions, layered and recast exceptions, etc,
> etc.
For guaranteed time/memory usage, take a look at something like the
statically typed Hume language...
http://www-fp.dcs.st-and.ac.uk/hume/
You might like to look at Epigram or other strongly normalizing languages
where you can't write an infinite loop...
http://www.e-pig.org/
http://lambda-the-ultimate.org/node/1120
...And take a look at Haskell's Software Transaction Memory to get rid of
dead-locks/race conditions...
http://research.microsoft.com/Users/simonpj/papers/stm/stm.pdf
"As we show, STM can be expressed particularly elegantly in a
declarative language, and we are able to use Haskell's type system to
give far stronger guarantees than are conventionally possible."
...also TyPiCal...
http://www.kb.ecei.tohoku.ac.jp/~koba/typical/
"TyPiCal is a type-based static analyzer for the pi-calculus. The
current version of TyPiCal provides four kinds of program analyses or
program transformations: lock-freedom analysis, deadlock-freedom
analysis, useless-code elimination, and information flow analysis."
...As for exceptions, give exception free programming a whirl...
http://www.haskell.org/pipermail/haskell-cafe/2006-September/017915.html
http://www.haskell.org/pipermail/haskell/2004-June/014271.html
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Robbert van Dalen — 2006-09-30 19:26:16
> I'm sorry that the executable and source code didn't
> work for you (is
> it because you don't have C#, and the .NET framework
> installed?). I
> appreciate the encouragement though.
Yeah, I'm a mac user. But I can read the source
because it's very clear (trying to execute it in my
head). Just read your blog - you have approached the
stage of unit testing. I guess that's the stage in
which Cat is getting seriously runnable ;)
> My focus on types is motivated by the fact that for
> non-trivial
> software (100,000 lines and plus) they become
> extremely important for
> catching errors early in the development process.
Hmm. I tend to disagree but that's my personal taste.
Anyway, tools that can bridge the communication
abysses between different departments are very useful
(such as type checkers or schema parser). Forcing
stricteness between interacting components is what
it's all about. I certainly would consider type
checking when interacting with components I didn't
develop :-)
> Typeless languages
> simply don't scale well for large projects.
I have this same feeling with Java, C++, Perl or any
language as a matter of fact. My feeling is that you
can only scale if you are absolutely succinct in every
possible way, conceptually or otherwise. That's where
the APL and K languages come to my mind.
> There aren't any mutable constructs in Cat. The
> notion of purity
> models whether a function has a dependency on an
> external state
OK, that's a somewhat different concept from what I
guessed from your documentation. Nevertheless,
allowing such dependencies in Cat does make it
contagious: one external state dependency can render
na entire Cat evalution to be dependent on external
state (which probably is the defaultf you consider an
keyboard input -> output loop).
> I hope this answers your questions?
Yes. But I ask for more answers! ;)
> Thanks again for your feedback and support,
> Christopher Diggins
Robbert.
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Rodney D Price — 2006-10-02 18:23:29
This discussion on static typing and type inference brings up
(in an indirect way) a question that I've been itching to ask for
some time. Haskell is a strongly typed language that can infer
almost all types in legal code. ML can infer all types -- the user
never has to provide a type annotation unless he or she wants
to. Both languages do this using the Hindley-Milner type
inference algorithm. What algorithm is Cat using, and what
guarantees do you have that your type inferencing is correct?
Along the same lines, about a month ago there was a discussion
on the Haskell-Cafe mailing list about so-called point-free style,
where a lambda term with named variables as arguments is
translated to a term without any arguments. For example
func :: (a -> Bool) -> (b -> a) -> [b] -> [a]
func f g l = filter f (map g l)
is a function that takes two functions f and g and a list l as
arguments.
The function g is mapped over l, then the elements of the resulting
list are filtered using f. (The first line is the type of func; the
second
is the definition.) Written in point-free style, we get
func = (. map) . (.) . filter
where "." is the function composition operator. There are no variables
here, only combinators. Any lambda term can be written in terms of
combinators; the translation can even be done automatically.
Haskell's point-free style appears to me to be concatenative (modulo
the infix syntax of "."). I say this because it's all just
combinators. If
Haskell indeed has a concatenative sub-language called "point-free
style", in which all terms can have their types inferred using Hindley-
Milner, then if you're designing a statically-typed concatenative
language, why not use Hindley-Milner? It's extremely powerful, and
known to be correct.
-Rod
On Sep 30, 2006, at 1:26 PM, Robbert van Dalen wrote:
>
> > I'm sorry that the executable and source code didn't
> > work for you (is
> > it because you don't have C#, and the .NET framework
> > installed?). I
> > appreciate the encouragement though.
> Yeah, I'm a mac user. But I can read the source
> because it's very clear (trying to execute it in my
> head). Just read your blog - you have approached the
> stage of unit testing. I guess that's the stage in
> which Cat is getting seriously runnable ;)
>
> > My focus on types is motivated by the fact that for
> > non-trivial
> > software (100,000 lines and plus) they become
> > extremely important for
> > catching errors early in the development process.
> Hmm. I tend to disagree but that's my personal taste.
> Anyway, tools that can bridge the communication
> abysses between different departments are very useful
> (such as type checkers or schema parser). Forcing
> stricteness between interacting components is what
> it's all about. I certainly would consider type
> checking when interacting with components I didn't
> develop :-)
>
> > Typeless languages
> > simply don't scale well for large projects.
> I have this same feeling with Java, C++, Perl or any
> language as a matter of fact. My feeling is that you
> can only scale if you are absolutely succinct in every
> possible way, conceptually or otherwise. That's where
> the APL and K languages come to my mind.
>
> > There aren't any mutable constructs in Cat. The
> > notion of purity
> > models whether a function has a dependency on an
> > external state
> OK, that's a somewhat different concept from what I
> guessed from your documentation. Nevertheless,
> allowing such dependencies in Cat does make it
> contagious: one external state dependency can render
> na entire Cat evalution to be dependent on external
> state (which probably is the defaultf you consider an
> keyboard input -> output loop).
>
> > I hope this answers your questions?
> Yes. But I ask for more answers! ;)
>
> > Thanks again for your feedback and support,
> > Christopher Diggins
>
> Robbert.
>
> __________________________________________________
> Do You Yahoo!?
> Tired of spam? Yahoo! Mail has the best spam protection around
> http://mail.yahoo.com
>
>
[Non-text portions of this message have been removed]
Christopher Diggins — 2006-10-03 01:34:07
On 10/2/06, Rodney D Price <
rodprice@...> wrote:
> This discussion on static typing and type inference brings up
> (in an indirect way) a question that I've been itching to ask for
> some time. Haskell is a strongly typed language that can infer
> almost all types in legal code. ML can infer all types -- the user
> never has to provide a type annotation unless he or she wants
> to. Both languages do this using the Hindley-Milner type
> inference algorithm. What algorithm is Cat using, and what
> guarantees do you have that your type inferencing is correct?
I created my own algorithm for type inferencing. I haven't proved
whether or not it is correct.
> Along the same lines, about a month ago there was a discussion
> on the Haskell-Cafe mailing list about so-called point-free style,
> where a lambda term with named variables as arguments is
> translated to a term without any arguments. For example
>
> func :: (a -> Bool) -> (b -> a) -> [b] -> [a]
> func f g l = filter f (map g l)
>
> is a function that takes two functions f and g and a list l as
> arguments.
> The function g is mapped over l, then the elements of the resulting
> list are filtered using f. (The first line is the type of func; the
> second
> is the definition.) Written in point-free style, we get
>
> func = (. map) . (.) . filter
>
> where "." is the function composition operator. There are no variables
> here, only combinators. Any lambda term can be written in terms of
> combinators; the translation can even be done automatically.
That is very interesting, I'd like to get my hands on that.
> Haskell's point-free style appears to me to be concatenative (modulo
> the infix syntax of "."). I say this because it's all just
> combinators. If
> Haskell indeed has a concatenative sub-language called "point-free
> style", in which all terms can have their types inferred using Hindley-
> Milner, then if you're designing a statically-typed concatenative
> language, why not use Hindley-Milner? It's extremely powerful, and
> known to be correct.
That is an interesting thought. I am not sure how much the H-M
algorithm differs from my own. I also don't know of any implementation
in C#. What I have is working fine for now, but if I run into any
insurmountable problems I will definitely consider H-M.
Thanks.
Christopher
William Tanksley, Jr — 2006-10-03 03:55:49
Rodney D Price <
rodprice@...> wrote:
> This discussion on static typing and type inference brings up
> (in an indirect way) a question that I've been itching to ask for
> some time. Haskell is a strongly typed language that can infer
> almost all types in legal code. ML can infer all types -- the user
> never has to provide a type annotation unless he or she wants
> to. Both languages do this using the Hindley-Milner type
> inference algorithm. What algorithm is Cat using, and what
> guarantees do you have that your type inferencing is correct?
I'm pretty sure -- but I may be wrong -- that you do sometimes have to
provide types in ML. IIRC, overloaded operators are the main culprit;
if there are others I've forgotten them.
> Along the same lines, about a month ago there was a discussion
> on the Haskell-Cafe mailing list about so-called point-free style,
> where a lambda term with named variables as arguments is
> translated to a term without any arguments. For example
> Haskell's point-free style appears to me to be concatenative (modulo
> the infix syntax of "."). I say this because it's all just
> combinators. If
Point-free style is combinator-based, and is commonly concatenative;
in particular, Haskell supports a concept called 'monads' which are
algebraicly the same as a (concatenative) stack.
Simpler words:
If you're using monads to write point-free code, you're probably concatenative.
But Haskell includes many other ways of writing point-free code --
simple function application is point-free if the functions are
themselves point-free.
> Haskell indeed has a concatenative sub-language called "point-free
> style", in which all terms can have their types inferred using Hindley-
> Milner, then if you're designing a statically-typed concatenative
> language, why not use Hindley-Milner? It's extremely powerful, and
> known to be correct.
H-M is very complex (NP complete? definitely 2^n in some situations),
and its complexity is needed for precisely the situations that
concatenative languages don't get into (lambdas). I don't know what
Cat is doing, but I always mention strongForth as having a nice
prototype of a type system with linear complexity. That's hard to
beat.
> -Rod
-Billy
Manfred Von Thun — 2006-10-03 07:57:46
On 3/10/06 4:23 AM, "Rodney D Price" <
rodprice@...> wrote:
>
>
> [..]
> Along the same lines, about a month ago there was a discussion
> on the Haskell-Cafe mailing list about so-called point-free style,
> where a lambda term with named variables as arguments is
> translated to a term without any arguments. For example
>
> func :: (a -> Bool) -> (b -> a) -> [b] -> [a]
> func f g l = filter f (map g l)
>
> is a function that takes two functions f and g and a list l as
> arguments.
> The function g is mapped over l, then the elements of the resulting
> list are filtered using f. (The first line is the type of func; the
> second
> is the definition.) Written in point-free style, we get
>
> func = (. map) . (.) . filter
>
> where "." is the function composition operator. There are no variables
> here, only combinators. Any lambda term can be written in terms of
> combinators; the translation can even be done automatically.
Thanks for that, Rodney.
In Joy: assuming that the top of the stack contains the list and
above that the two quotations [g] [f], with [f] topmost,
then the definition is
func == [map] dip filter
or in this particular case, where map is before filter:
func == [b] cons cons filter
func == concat filter
(this does not work if filter is before map).
[Non-text portions of this message have been removed]
Rodney D Price — 2006-10-09 17:23:52
Sorry for the delayed response. I've been out of town and out of touch.
> [snip]
> > is the definition.) Written in point-free style, we get
> >
> > func = (. map) . (.) . filter
> >
> > where "." is the function composition operator. There are no
> variables
> > here, only combinators. Any lambda term can be written in terms of
> > combinators; the translation can even be done automatically.
>
> That is very interesting, I'd like to get my hands on that.
An implementation can be found in a plugin for the LambdaBot tool. See
http://www.cse.unsw.edu.au/~dons/lambdabot.html
> > Haskell's point-free style appears to me to be concatenative (modulo
> > the infix syntax of "."). I say this because it's all just
> > combinators. If
> > Haskell indeed has a concatenative sub-language called "point-free
> > style", in which all terms can have their types inferred using
> Hindley-
> > Milner, then if you're designing a statically-typed concatenative
> > language, why not use Hindley-Milner? It's extremely powerful, and
> > known to be correct.
>
> That is an interesting thought. I am not sure how much the H-M
> algorithm differs from my own. I also don't know of any implementation
> in C#. What I have is working fine for now, but if I run into any
> insurmountable problems I will definitely consider H-M.
>
> Thanks.
> Christopher
C# 3.0 is supposed to include some type inferencing capability. I've
heard
that it will use Hindley-Milner. See
http://en.wikipedia.org/wiki/C_Sharp#C.23_3.0_new_language_features
-Rod
Rodney D Price — 2006-10-09 17:43:52
Here's a paragraph in Benjamin Pierce's "Advanced Topics in
Types and Programming Languages," p.391, that may clarify
some of the issues brought up below:
"... type inference for [Hindley-Milner] is known to be DEXPTIME-
complete. In practice, however, most implementations of it
behave well. This apparent contradiction may be explained by
observing that types usually remain small and that let constructs
are never deeply nested toward the left. Indeed, under the
assumption that types have bounded size and that programs
have bounded "scheme-depth", type inference may be performed
in quasi-linear time."
There's also the fact that Haskell, ML, etc have been using Hindley-
Milner for many years now, and that it works very well.
More comments in-line below.
On Oct 2, 2006, at 9:55 PM, William Tanksley, Jr wrote:
> Rodney D Price <rodprice@...> wrote:
> > This discussion on static typing and type inference brings up
> > (in an indirect way) a question that I've been itching to ask for
> > some time. Haskell is a strongly typed language that can infer
> > almost all types in legal code. ML can infer all types -- the user
> > never has to provide a type annotation unless he or she wants
> > to. Both languages do this using the Hindley-Milner type
> > inference algorithm. What algorithm is Cat using, and what
> > guarantees do you have that your type inferencing is correct?
>
> I'm pretty sure -- but I may be wrong -- that you do sometimes have to
> provide types in ML. IIRC, overloaded operators are the main culprit;
> if there are others I've forgotten them.
There are many variants of ML, that often implement extensions to
Hindley-Milner. If the compiler sticks to standard Hindley-Milner
inference, all types can be inferred.
>
> > Along the same lines, about a month ago there was a discussion
> > on the Haskell-Cafe mailing list about so-called point-free style,
> > where a lambda term with named variables as arguments is
> > translated to a term without any arguments. For example
>
> > Haskell's point-free style appears to me to be concatenative (modulo
> > the infix syntax of "."). I say this because it's all just
> > combinators. If
>
> Point-free style is combinator-based, and is commonly concatenative;
> in particular, Haskell supports a concept called 'monads' which are
> algebraicly the same as a (concatenative) stack.
Monads and point-free style are entirely orthogonal concepts. Monads
in Haskell are a means to support side effects, state, etc in a purely
referentially transparent language. Point-free style is just a way of
making function definitions without using explicit arguments.
If you can show that monads *are* algebraically the same as a
concatenative stack, as you say, you should write a paper. It would get
a lot of attention in the functional programming community. I would be
very (pleasantly) surprised if that were true, however.
>
> Simpler words:
>
> If you're using monads to write point-free code, you're probably
> concatenative.
>
> But Haskell includes many other ways of writing point-free code --
> simple function application is point-free if the functions are
> themselves point-free.
Trivially true given the definition above. In this context, a
combinator is
nothing more than a function with no free variables.
> > Haskell indeed has a concatenative sub-language called "point-free
> > style", in which all terms can have their types inferred using
> Hindley-
> > Milner, then if you're designing a statically-typed concatenative
> > language, why not use Hindley-Milner? It's extremely powerful, and
> > known to be correct.
>
> H-M is very complex (NP complete? definitely 2^n in some situations),
> and its complexity is needed for precisely the situations that
> concatenative languages don't get into (lambdas). I don't know what
> Cat is doing, but I always mention strongForth as having a nice
> prototype of a type system with linear complexity. That's hard to
> beat.
StrongForth doesn't do type inference, as far as I know. Am I wrong? I
just gave a StrongForth paper a quick read many months ago.
At any rate, real, provably correct type inference is hard to beat.
-Rod
>
> > -Rod
>
> -Billy
>
>
Rodney D Price — 2006-10-09 17:53:34
Manfred,
Thanks for your response. This is certainly a lot more readable
than the Haskell point-free version. My purpose in giving a
Haskell version was to present evidence that a combinator-
based, presumably concatenative language could be statically
typed. I seem to remember seeing claims that Joy cannot be
typed, or at the very least, that Joy must be dynamically typed.
Is this true?
-Rod
>
> In Joy: assuming that the top of the stack contains the list and
> above that the two quotations [g] [f], with [f] topmost,
> then the definition is
> func == [map] dip filter
> or in this particular case, where map is before filter:
> func == [b] cons cons filter
> func == concat filter
> (this does not work if filter is before map).
>
Greg Buchholz — 2006-10-10 18:12:19
Paul-V Khuong — 2006-10-10 22:56:14
"Rodney D Price" writes:
> Thanks for your response. This is certainly a lot more readable
> than the Haskell point-free version. My purpose in giving a
> Haskell version was to present evidence that a combinator-
> based, presumably concatenative language could be statically
> typed. I seem to remember seeing claims that Joy cannot be
> typed, or at the very least, that Joy must be dynamically typed.
> Is this true?
Yes, a certain subset of concatenative languages can be mapped to
first-order functional (ok, pure) programs: those for which you have
words of known arity both in and out (and apply based on tuples, not
list, I think). Obviously, if you want to use HM, you can't have ad-hoc
polymorphism. If you want to type legacy Forth code, though, your
job is a priori much worse than that facing people who check C
statically (a stack frame shift has a global effect and is hard to detect,
unlike passing extra or not enough arguments to a C function). In fact,
I still haven't found a way to extract reasonable constraints out of
arbitrary Forth programs
Paul Khuong
Manfred Von Thun — 2006-10-13 08:35:17
On 10/10/06 3:53 AM, "Rodney D Price" <
rodprice@...> wrote:
>
> Manfred,
>
> Thanks for your response. This is certainly a lot more readable
> than the Haskell point-free version. My purpose in giving a
> Haskell version was to present evidence that a combinator-
> based, presumably concatenative language could be statically
> typed. I seem to remember seeing claims that Joy cannot be
> typed, or at the very least, that Joy must be dynamically typed.
> Is this true?
>
> -Rod
About the Haskell version: does it really work for all lists? what if there
are different types of element in the list in the simplest case, suppose
there are integers, floats and strings in the list, and the function ([f]
from memory) to be mapped was essentially:
> if it is an integer, leave it as it is
> if it is a float, take its square
> if it is a string, read it as a number and treat as above
and the other function ([g] from memory) for filtering was
> is the number greater than 42 ?
Does this really work in Haskell¹s type system? I do not understand
Haskell well enough to know.
Joy is in fact weakly and dynamically typed. Whether it can be
statically typed has been discussed on this group, and from memory
it was not really settled. Part of the NO-argument seemed to be that
the stack must be heterogeneous to hold all sorts of things, but that
lists should be homogeneous. Another part of the NO-argument was
that the size of the stack was not predictable at compile time and
hence the type of its elements could not be known at compile time.
I think there was also converse argument that to make such things
known at compile time certain operations should be forbidden
which now are allowed. Whether these inferences really hold I
am still uncertain about. One important feature about the stack and
lists is that the stack is just a list that is the central focus of
attention,
for the program writer, the reader, and the Joy interpreter. Much of
Joy depends on the stack being just a list, and whatever is OK for
lists should be OK for the stack.
Writing a small version of Joy in Haskell would go a long way
towards settling some of these arguments.
- Manfred
[Non-text portions of this message have been removed]
John Cowan — 2006-10-13 15:03:32
Manfred Von Thun scripsit:
> About the Haskell version: does it really work for all lists? what if
> there are different types of element in the list in the simplest
> case, suppose there are integers, floats and strings in the list,
> and the function ([f] from memory) to be mapped was essentially:
Haskell, like other ML-derived languages, has only homogeneous lists, though
the inconvenience of this is somewhat reduced in Haskell due to the
invention of type classes (essentially like OO interfaces).
--
Not to perambulate John Cowan <
cowan@...>
the corridors
http://www.ccil.org/~cowan
during the hours of repose
in the boots of ascension. --Sign in Austrian ski-resort hotel
Christopher Diggins — 2006-10-13 15:28:10
One of the biggest challenges in making Joy type safe is that functions can
be created at runtime. Calling "i" on one of these functions would leave the
stack in a state which can not be determined (in the general case) at
compile time. This undercuts the purpose of a static type system: to
determine a program state statically in terms of types, and assure that the
behaviour is as expected (which means you need to have some kind of type
annotation to compare the type against).
You can still have a partially decidable type system I believe, and it would
still be useful. You just need to enter variable types (variants) where the
types can not be known a-priori. When entire chunks of a stack can not be
computed in advance, perhaps another form of variant which stands for
multiple types could be used.
I have been designing Cat to be completely decidable at compile-time, but I
am not convinced that it is neccessary.
For those interested in discussions related to static type-checking of
dynamically typed languages should check out
http://www.lambda-the-ultimate.org
On 10/13/06, Manfred Von Thun <m.vonthun@...> wrote:
>
>
> On 10/10/06 3:53 AM, "Rodney D Price" <rodprice@...<rodprice%40raytheon.com>>
> wrote:
> >
> > Manfred,
> >
> > Thanks for your response. This is certainly a lot more readable
> > than the Haskell point-free version. My purpose in giving a
> > Haskell version was to present evidence that a combinator-
> > based, presumably concatenative language could be statically
> > typed. I seem to remember seeing claims that Joy cannot be
> > typed, or at the very least, that Joy must be dynamically typed.
> > Is this true?
> >
> > -Rod
>
> About the Haskell version: does it really work for all lists? what if
> there
> are different types of element in the list in the simplest case, suppose
> there are integers, floats and strings in the list, and the function ([f]
> from memory) to be mapped was essentially:
>
> > if it is an integer, leave it as it is
> > if it is a float, take its square
> > if it is a string, read it as a number and treat as above
>
> and the other function ([g] from memory) for filtering was
>
> > is the number greater than 42 ?
>
> Does this really work in Haskell¹s type system? I do not understand
> Haskell well enough to know.
>
> Joy is in fact weakly and dynamically typed. Whether it can be
> statically typed has been discussed on this group, and from memory
> it was not really settled. Part of the NO-argument seemed to be that
> the stack must be heterogeneous to hold all sorts of things, but that
> lists should be homogeneous. Another part of the NO-argument was
> that the size of the stack was not predictable at compile time and
> hence the type of its elements could not be known at compile time.
> I think there was also converse argument that to make such things
> known at compile time certain operations should be forbidden
> which now are allowed. Whether these inferences really hold I
> am still uncertain about. One important feature about the stack and
> lists is that the stack is just a list that is the central focus of
> attention,
> for the program writer, the reader, and the Joy interpreter. Much of
> Joy depends on the stack being just a list, and whatever is OK for
> lists should be OK for the stack.
>
> Writing a small version of Joy in Haskell would go a long way
> towards settling some of these arguments.
>
> - Manfred
>
> [Non-text portions of this message have been removed]
>
>
>
[Non-text portions of this message have been removed]
William Tanksley, Jr — 2006-10-13 22:47:30
Rodney D Price <
rodprice@...> wrote:
> On Oct 2, 2006, at 9:55 PM, William Tanksley, Jr wrote:
> > > Along the same lines, about a month ago there was a discussion
> > > on the Haskell-Cafe mailing list about so-called point-free style,
> > > where a lambda term with named variables as arguments is
> > > translated to a term without any arguments. For example
> > > Haskell's point-free style appears to me to be concatenative (modulo
> > > the infix syntax of "."). I say this because it's all just
> > > combinators. If
> > Point-free style is combinator-based, and is commonly concatenative;
> > in particular, Haskell supports a concept called 'monads' which are
> > algebraicly the same as a (concatenative) stack.
> Monads and point-free style are entirely orthogonal concepts. Monads
> in Haskell are a means to support side effects, state, etc in a purely
> referentially transparent language. Point-free style is just a way of
> making function definitions without using explicit arguments.
Side effects are reasonably handled within monad code because the
sequence of evaluation for monad code is strictly defined (it's not in
general for functional code). Monads aren't merely "a means to support
side effects"; they're a mathematical concept that, among other
things, allow you to express side effects withhout losing other nice
benefits of a mathematical language.
> If you can show that monads *are* algebraically the same as a
> concatenative stack, as you say, you should write a paper. It would get
> a lot of attention in the functional programming community. I would be
> very (pleasantly) surprised if that were true, however.
That was a typo on my part -- I meant it the other way around.
> > Simpler words:
> >
> > If you're using monads to write point-free code, you're probably
> > concatenative.
> >
> > But Haskell includes many other ways of writing point-free code --
> > simple function application is point-free if the functions are
> > themselves point-free.
> Trivially true given the definition above.
"But Haskell includes..." is not "trivially true". I was giving a
simple example of one of the ways you can be point-free, under the
heading of "simpler words". I.e. I'm trying to be clearer for people
without quite so much schooling in Haskell.
> In this context, a
> combinator is nothing more than a function with no free variables.
Right -- a nice way to be point-free.
> > > Milner, then if you're designing a statically-typed concatenative
> > > language, why not use Hindley-Milner? It's extremely powerful, and
> > > known to be correct.
> > H-M is very complex (NP complete? definitely 2^n in some situations),
> > and its complexity is needed for precisely the situations that
> > concatenative languages don't get into (lambdas). I don't know what
> > Cat is doing, but I always mention strongForth as having a nice
> > prototype of a type system with linear complexity. That's hard to
> > beat.
> StrongForth doesn't do type inference, as far as I know. Am I wrong? I
> just gave a StrongForth paper a quick read many months ago.
Nope -- but I thought we were asking about static typing, not type inference.
StrongForth is a good demo of the lengths you have to go to in order
to get strong static typing on an ANSI Forth core. Not always
pleasant. The same system built on a non-ANSIForth would/could be much
cleaner.
One thing you can do on a dynamicly typed stack that you can't do on a
static one: variable-depth iteration. Personally, I think a good cure
for this would be to let the stack be static, and user vector/array
operations (like APL/J/K) for the dynamic stuff.
> At any rate, real, provably correct type inference is hard to beat.
Hard to argue with that! I agree.
> -Rod
-Billy
John Cowan — 2006-10-13 22:54:50
William Tanksley, Jr scripsit:
> > At any rate, real, provably correct type inference is hard to beat.
>
> Hard to argue with that! I agree.
The argument is: are the benefits worth the costs?
--
In politics, obedience and support John Cowan <
cowan@...>
are the same thing. --Hannah Arendt
http://www.ccil.org/~cowan
William Tanksley, Jr — 2006-10-14 22:53:19
John Cowan <
cowan@...> wrote:
> William Tanksley, Jr scripsit:
> > > At any rate, real, provably correct type inference is hard to beat.
> > Hard to argue with that! I agree.
> The argument is: are the benefits worth the costs?
A worthy question. Depends on how you parse out the "costs". If losing
dynamic typing is a cost to you, then I don't think ANY benefits of
type inference could outweigh it for you. If you're already planning
to use static typing, though, the cost would probably come down to
more complexity in your compiler... Each compiler implementor will
have to make a judgement call on that.
Do you see some other cost I'm missing?
> In politics, obedience and support John Cowan <cowan@...>
-Billy
John Cowan — 2006-10-14 23:55:28
William Tanksley, Jr scripsit:
> A worthy question. Depends on how you parse out the "costs". If losing
> dynamic typing is a cost to you, then I don't think ANY benefits of
> type inference could outweigh it for you.
Type inference can be supplemented by explicit typing or even explicit
dynamic typing (e.g. Variant variables in Visual Basic).
It's really about which combination of mechanisms you want to support:
ML can infer almost all types but lets you specify types so you
can do ad-hoc polymorphism on +, -, etc. Haskell's type classes
eliminate the need for that. Java provides only explicit static
typing with the exception of dynamic casts. Etc.
> If you're already planning
> to use static typing, though, the cost would probably come down to
> more complexity in your compiler... Each compiler implementor will
> have to make a judgement call on that.
Indeed.
--
John Cowan <
cowan@...>
Yakka foob mog. Grug pubbawup zink wattoom gazork. Chumble spuzz.
-- Calvin, giving Newton's First Law "in his own words"
Rodney D Price — 2006-10-16 17:03:11
I like to think of the static typing vs dynamic typing issue this way:
Suppose that you had a dynamically typed language that you
were quite happy with. Now suppose that someone wrote a lint-
like package for your language that caught *all* typing errors up
front, before you ever ran your code. That is, the lint program
would provide you with a proof that you would never see a run-
time type error. Would you want to use it, or not?
Many programmers would immediately object that it's impossible
to write such a package; or rather, that it's impossible to write such
a package for the particular dynamic features that they like most.
I would respond that most programmers haven't seen how much
an advanced type system can do. For an example, have a look at
the dynamic plugin architecture in this paper, at
http://www.cse.unsw.edu.au/~dons/papers/SC05.html
In the context of concatenative languages, it appears to me that
there is a unique opportunity for static typing with type inference.
Concatenative languages are above all simple. Given all the
work that has gone into type systems over the past 30 years, it
should be possible to design a concatenative language with
full type inference. Perhaps a small variation on Joy would do.
Then you'd really have the lint tool above.
OTOH, some years ago I ran a small R&D project where we used
Haskell's type system to provide guarantees of some behavior
necessary for fault tolerant behavior. I was given two C program-
mers to help, and I had to teach them Haskell. After a few weeks
of struggle, my two programmers openly rebelled. The problem
was this: they were extremely frustrated with the fact that most of
their code would not type-check. They wanted to write code off
the top of their heads and weed out the bugs by testing. When
the compiler told them up front that their code was wrong, they
found that they had to pick through their code by hand to find the
errors. They didn't want to do that -- they wanted to get something
"working" fast, then use their familiar debugging tools to fix things.
(Not that C is a dynamic language... but compared to a modern
type system like Haskell's, it almost doesn't have a type system.
Many, many errors get past the C type system that would be
caught by better type systems like Haskell's.)
-Rod
On Oct 14, 2006, at 5:55 PM, John Cowan wrote:
> William Tanksley, Jr scripsit:
>
> > A worthy question. Depends on how you parse out the "costs". If
> losing
> > dynamic typing is a cost to you, then I don't think ANY benefits of
> > type inference could outweigh it for you.
>
> Type inference can be supplemented by explicit typing or even explicit
> dynamic typing (e.g. Variant variables in Visual Basic).
> It's really about which combination of mechanisms you want to support:
> ML can infer almost all types but lets you specify types so you
> can do ad-hoc polymorphism on +, -, etc. Haskell's type classes
> eliminate the need for that. Java provides only explicit static
> typing with the exception of dynamic casts. Etc.
>
> > If you're already planning
> > to use static typing, though, the cost would probably come down to
> > more complexity in your compiler... Each compiler implementor will
> > have to make a judgement call on that.
>
> Indeed.
>
> --
> John Cowan <cowan@...>
> Yakka foob mog. Grug pubbawup zink wattoom gazork. Chumble spuzz.
> -- Calvin, giving Newton's First Law "in his own words"
>
>
[Non-text portions of this message have been removed]
Rodney D Price — 2006-10-16 18:15:04
This is very interesting. I had thought of using Haskell's type classes
to build a list that could be used as a stack, but that really
defeats the
purpose of the exercise. I also thought of using Haskell's existential
types, but I don't understand them that well, and they seemed to have
the same objection (no real typing of the stack) as the type class
approach.
You use nested tuples, taking advantage of Haskell's parametric
polymorphism to type the stack. That's not crude, that's ingenious!
I do have a question about your folds, however. Your fold appears
to operate only on a single list on the stack. Granted, that is en-
compasses any recursive operator over that list, but does it really
include recursion over (or using) the stack?
-Rod
On Oct 10, 2006, at 12:12 PM, Greg Buchholz wrote:
> --- Rodney D Price <rodprice@...> wrote:
> > My purpose in giving a
> > Haskell version was to present evidence that a combinator-
> > based, presumably concatenative language could be statically
> > typed.
>
> Here are a couple of very crude examples which I started experimenting
> with a while back to convince myself a statically typed
> concatenative/stack-based language was possible. One is in Haskell and
> the other, C++. (Once you've got "fold" and "unfold" you get general
> recursion for free. http://citeseer.ist.psu.edu/293490.html ).
>
> http://sleepingsquirrel.org/joy/typed_joy.hs
> http://sleepingsquirrel.org/joy/template_joy.cpp
>
> Greg Buchholz
>
> __________________________________________________
> Do You Yahoo!?
> Tired of spam? Yahoo! Mail has the best spam protection around
> http://mail.yahoo.com
>
>
[Non-text portions of this message have been removed]
Greg Buchholz — 2006-10-17 04:15:32
--- Rodney D Price <
rodprice@...> wrote:
>
> I do have a question about your folds, however. Your fold appears
> to operate only on a single list on the stack. Granted, that is en-
> compasses any recursive operator over that list, but does it really
> include recursion over (or using) the stack?
>
No? I'm not sure I fully understand your question. I just
implemented "fold" and "unfold" over lists, instead of coming up with a
statically typable version of "linrec" or "genrec" working over the
stack, because it seemed easier at the time. Just think of the
intermediate list as the return value stack. It seems like a pretty
reasonable thing to do, since we want static typing. If that seems too
restrictive, we could use nested data types and polymorphic recursion, if
we are willing to put up with type annotations, or use a more powerful
type system than found in Haskell.
Trying to define something like "linrec" in Haskell in the same obvious
way you would in Joy results in problems with the occurs check in the
type inferencer. Maybe switching to O'Caml would be better since it
omits the occurs check.
Greg Buchholz
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Greg Buchholz — 2006-10-22 06:45:29
--- John Cowan <
cowan@...> wrote:
] Manfred Von Thun scripsit:
]
] ] About the Haskell version: does it really work for all lists? what if
] ] there are different types of element in the list in the simplest
] ] case, suppose there are integers, floats and strings in the list,
] ] and the function ([f] from memory) to be mapped was essentially:
]
] Haskell, like other ML-derived languages, has only homogeneous lists,
] though the inconvenience of this is somewhat reduced in Haskell due to
] the invention of type classes (essentially like OO interfaces).
In theory, that's true. In practice, there's a lot you can do to
eat your heterogeneous list cake, while still having it. The real
limitation of a statically typed language like Haskell is that you can't
have an arbitrarily ordered list of arbitrary elements with an arbitrary
length, without having run-time tags. If you relax some of those
restrictions, you can get close to heterogeneous lists. (This message
is literate Haskell code, you can save it in a file and load it into the
Haskell compiler/interpreter of your choice. Try "ghci message.lhs" or
"hugs -98 message.lhs".) Here's some initialization boilerplate we need
to get out of the way...
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> import Data.Dynamic
...The most obvious solution is to create an new data type which can
hold integers, floating point numbers, or strings...
> data IFS = I Integer | F Double | S String deriving Show
> ifs = [I 4, F 5.0, S "6", F 7.0]
...with that (also known as a discriminated union), you can have lists
of indeterminate length and any ordering of Integers, Doubles, or
Strings. The downside is of course that you are stuck with only having
Integers, Doubles, or Strings, and the values are tagged with the
I,F,and S constructors. This is essentially the dynamic typing
solution, and if your functions don't cover all the possible cases, you
could get run time errors.
If you don't want to be limited to a statically known set of
types in the union, you can use something like the Data.Dynamic
library...
http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Dynamic.html
...which is similar to having a data type with (almost) all possible
cases built in...
> dynamic = [toDyn (4::Int),toDyn (5.0::Double),toDyn ("6"::String)]
...If we know that the elements we want to stick in a list all support
the same interface, we could also use an existential type to hide the
representation...
> data Existential = forall a . (Show a) => Ex a
> ex = [Ex 4, Ex 5.0, Ex "6"]
...this allows us to have an arbitrary length list with elements in any
order, but there have to be some common functions which can operate on
the values. In the above case, all elements have to be supported by the
function "show", which turns a value into a string. And it is a one-way
street, since we can't really do anything with the individual elements,
other than apply our common functions to them.
If we don't need to have lists of statically unknown length, we
could instead use nested tuples...
> tuples = (4,(5.0,"6"))
...Now you can stick anything in there, without tagging, but the overall
structure has to be statically known. See also, the paper...
Strongly typed heterogeneous collections
http://homepages.cwi.nl/~ralf/HList/
Or if we know some relation concerning the ordering of our elements,
we can make a (possibly) infinite data structure custom tailored to hold
them. If we know that we'll always have an Integer, followed by a
Double, followed by a String, we could use something like...
> data Twist a b c = TNil | TCons a (Twist b c a) deriving Show
> twist = TCons 4 (TCons 5.0 (TCons "6" TNil))
...or if we know that we've got one integer, then two strings, then
three integers, then four strings, etc.
> data Fancy a b left next =
> forall c d left' next' lz decleft .
> (Show c, Show d,
> Zerop left lz,
> If lz (Succ next) next next',
> Pre left decleft,
> If lz next decleft left',
> If lz b a c,
> If lz a b d
> ) => Cons a (Fancy c d left' next') | Nil
>
> fancy :: Fancy Integer String Zero (Succ Zero)
> fancy = (Cons 1
> (Cons "a" (Cons "b"
> (Cons 2 (Cons 3 (Cons 4
> (Cons "c" (Cons "d" (Cons "e" (Cons "f"
> (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9
Nil)))))))))))))))
...see "Fun with Functional Dependencies"...
http://www.cs.chalmers.se/~hallgren/Papers/wm01.html
...to learn more about performing computations with the type system.
Finally, here's something a little bit strange. It is a list of a
Double, followed by a function of (Double -> Double), followed by a
function of ((Double -> Double) -> (Double -> Double)), followed by
((Double -> Double) -> (Double -> Double)) -> ((Double -> Double) ->
(Double -> Double)), etc.
> data Funcs a = Fun a (Funcs (a -> a)) | FNil
> funcs = Fun 1 (Fun (2 /) (Fun (\x y -> x y * 3) (Fun id FNil)))
Of course, you can also combine these techniques...
> combined = (Fun ((TCons fancy (TCons ex (TCons funcs TNil))),
> (dynamic, ifs)) (Fun id FNil))
...And here are some of the helper functions needed for the above
code...
> instance (Show a, Show b) => Show (Fancy a b c d) where
> show (Cons x xs) = "(Cons " ++ (show x) ++ " " ++ (show xs) ++ ")"
> show Nil = "Nil"
>
> instance Show a => Show (Funcs a) where
> show (Fun x xs) = "(Fun " ++ show x ++ " " ++ show xs ++ ")"
> show FNil = "FNil"
>
> instance Show (a -> b) where show _ = "<function>"
>
> data Succ a
> data Zero
>
> data TTrue
> data TFalse
>
> class Pre a b | a -> b
> instance Pre (Succ a) a
> instance Pre Zero Zero
>
> class If p t e result | p t e -> result
> instance If TTrue a b a
> instance If TFalse a b b
>
> class Zerop a b | a -> b
> instance Zerop Zero TTrue
> instance Zerop (Succ a) TFalse
>
> instance Show Existential where show (Ex x) = show x
__________________________________________________
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Greg Buchholz — 2006-10-22 07:24:33