I've written a short article explaining how to infer the types using
the example of a non-trivial higher order function: "[] eval eval" at
http://cdiggins.com/2007/04/11/type-inference-example-in-cat/ for
those interested in a more down to earth explanation of the type
inference algorithm.
Cheers,
Christopher Diggins
http://www.cdiggins.com
A perhaps trivial question [which also serves to test if my - via
gmail - posts get through] is: "is it obvious why one would
want to 'infer the types' ?"
== Chris Glur.
On 4/11/07, Christopher Diggins <cdiggins@...> wrote:
> I've written a short article explaining how to infer the types using
> the example of a non-trivial higher order function: "[] eval eval" at
> http://cdiggins.com/2007/04/11/type-inference-example-in-cat/ for
> those interested in a more down to earth explanation of the type
> inference algorithm.
>
> Cheers,
> Christopher Diggins
> http://www.cdiggins.com
>
chris glur <crglur@...> wrote:
> A perhaps trivial question [which also serves to test if my - viaMaybe not.
> gmail - posts get through] is: "is it obvious why one would
> want to 'infer the types' ?"
There are many languages that do very little typechecking at compile
time. They include concatenative languages like Forth, Joy, and
Postscript; people have worked with them for years. The problem is
that many errors you can make in them are incredibly hard to narrow
down and find, but very easy to make. You'd think that with just a
little tiny bit of static checking you could prevent a huge, annoying
class of problems from ever becoming an error.
The problem then becomes that the programmer has to tell the compiler
all about the types of the programs he wants to write, even though
"types" are not what programming is supposed to be about.
Type Inferencing makes the compiler do a bit of work to figure out
what the programmer meant, assuming that the programmer wanted to
write a program that behaves consistently and predictably. As a bonus,
not only does the programmer NOT have to explain all the types to the
compiler, the programmer also gets an error from the compiler if his
program isn't going to behave consistently and predictably.
> == Chris Glur.-Billy
This question implies the question "why would one want to statically verify
the types?". This one is fairly well-known: e.g. documentation, reducing
defects, and improving performance, so I'll assume that it is already known.
The question that remains then is "why allow the compiler (or better yet,
the editor) infer the types instead of insisting the programmer write them
out?".
If you want static type verification then you will encounter a fair number
of scenarios where expressing the types is non-trivial and the type
signature may even be longer than the function body. Sometimes the type is
not easily deduced by a programmer due to lack of familiarity with the
complexities of type systems, but the programmer still knows how to write
the program they want correctly. Finally, there are scenarios where the type
is so trivially obvious, writing it is redundant.
As for whether or not it is obvious, that really depends on your experience
with statically typed languages, and an understanding of how the refactoring
capabilities of modern IDEs for C# and Java actually do their magic. The
more type inference you are able to do with a langauge, the more an IDE can
refactor your code for you.
Hope this helps.
Christopher Diggins
On 4/16/07, chris glur <crglur@...> wrote:
>
> A perhaps trivial question [which also serves to test if my - via
> gmail - posts get through] is: "is it obvious why one would
> want to 'infer the types' ?"
>
> == Chris Glur.
>
> On 4/11/07, Christopher Diggins <cdiggins@... <cdiggins%40gmail.com>>
> wrote:
> > I've written a short article explaining how to infer the types using
> > the example of a non-trivial higher order function: "[] eval eval" at
> > http://cdiggins.com/2007/04/11/type-inference-example-in-cat/ for
> > those interested in a more down to earth explanation of the type
> > inference algorithm.
> >
> > Cheers,
> > Christopher Diggins
> > http://www.cdiggins.com
> >
>
> Messages in this topic
> <http://groups.yahoo.com/group/concatenative/message/3297;_ylc=X3oDMTM0amE5dGJzBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzMyOTgEc2VjA2Z0cgRzbGsDdnRwYwRzdGltZQMxMTc2NzEzOTgxBHRwY0lkAzMyOTc->
> (0) Reply (via web post)
> <http://groups.yahoo.com/group/concatenative/post;_ylc=X3oDMTJwN21kbjhqBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzMyOTgEc2VjA2Z0cgRzbGsDcnBseQRzdGltZQMxMTc2NzEzOTgx?act=reply&messageNum=3298>|
> Start a new topic
> <http://groups.yahoo.com/group/concatenative/post;_ylc=X3oDMTJlNjZ1Y2Y4BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA250cGMEc3RpbWUDMTE3NjcxMzk4MQ-->
> Messages<http://groups.yahoo.com/group/concatenative/messages;_ylc=X3oDMTJlbGJqMzZhBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA21zZ3MEc3RpbWUDMTE3NjcxMzk4MQ-->|
> Files<http://groups.yahoo.com/group/concatenative/files;_ylc=X3oDMTJmYzUwaW8yBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2ZpbGVzBHN0aW1lAzExNzY3MTM5ODE->|
> Photos<http://groups.yahoo.com/group/concatenative/photos;_ylc=X3oDMTJldTM2NG9jBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA3Bob3QEc3RpbWUDMTE3NjcxMzk4MQ-->|
> Links<http://groups.yahoo.com/group/concatenative/links;_ylc=X3oDMTJmMjdvYTR0BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2xpbmtzBHN0aW1lAzExNzY3MTM5ODE->|
> Database<http://groups.yahoo.com/group/concatenative/database;_ylc=X3oDMTJjOGx0NjhyBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2RiBHN0aW1lAzExNzY3MTM5ODE->|
> Polls<http://groups.yahoo.com/group/concatenative/polls;_ylc=X3oDMTJmMjZ2dDh0BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA3BvbGxzBHN0aW1lAzExNzY3MTM5ODE->|
> Members<http://groups.yahoo.com/group/concatenative/members;_ylc=X3oDMTJlbGdkNWliBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA21icnMEc3RpbWUDMTE3NjcxMzk4MQ-->|
> Calendar<http://groups.yahoo.com/group/concatenative/calendar;_ylc=X3oDMTJkdTE2cThhBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2NhbARzdGltZQMxMTc2NzEzOTgx>
> [image: Yahoo! Groups]<http://groups.yahoo.com/;_ylc=X3oDMTJkdHJwc3BmBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2dmcARzdGltZQMxMTc2NzEzOTgx>
> Change settings via the Web<http://groups.yahoo.com/group/concatenative/join;_ylc=X3oDMTJmOXNxaGhxBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA3N0bmdzBHN0aW1lAzExNzY3MTM5ODE->(Yahoo! ID required)
> Change settings via email: Switch delivery to Daily Digest<concatenative-digest@yahoogroups.com?subject=Email+Delivery:+Digest>| Switch
> format to Traditional<concatenative-traditional@yahoogroups.com?subject=Change+Delivery+Format:+Traditional>
> Visit Your Group
> <http://groups.yahoo.com/group/concatenative;_ylc=X3oDMTJkNmtiaHZyBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2hwZgRzdGltZQMxMTc2NzEzOTgx>|
> Yahoo! Groups Terms of Use <http://docs.yahoo.com/info/terms/>| Unsubscribe
> <concatenative-unsubscribe@yahoogroups.com?subject=>
> Visit Your Group
> <http://groups.yahoo.com/group/concatenative;_ylc=X3oDMTJlaGI2NnBpBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwN2dGwEc2xrA3ZnaHAEc3RpbWUDMTE3NjcxMzk4MQ-->
> SPONSORED LINKS
>
> - Computer telephony<http://groups.yahoo.com/gads;_ylc=X3oDMTJjYnZubHU1BF9TAzk3MzU5NzE0BF9wAzEEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA3NsbW9kBHN0aW1lAzExNzY3MTM5ODE-?t=ms&k=Computer+telephony&w1=Computer+telephony&w2=Portable+computer&w3=Portable+computer+case&w4=Computer+telephony+integration&w5=Computer+telephony+integration+cti&c=5&s=151&g=2&.sig=JAsp-14TIOM--smLD8umaA>
> - Portable computer<http://groups.yahoo.com/gads;_ylc=X3oDMTJjZWptOHVnBF9TAzk3MzU5NzE0BF9wAzIEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA3NsbW9kBHN0aW1lAzExNzY3MTM5ODE-?t=ms&k=Portable+computer&w1=Computer+telephony&w2=Portable+computer&w3=Portable+computer+case&w4=Computer+telephony+integration&w5=Computer+telephony+integration+cti&c=5&s=151&g=2&.sig=MJdJLwRbIl1obm3uSH-5JQ>
> - Portable computer case<http://groups.yahoo.com/gads;_ylc=X3oDMTJjN2I2amYzBF9TAzk3MzU5NzE0BF9wAzMEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA3NsbW9kBHN0aW1lAzExNzY3MTM5ODE-?t=ms&k=Portable+computer+case&w1=Computer+telephony&w2=Portable+computer&w3=Portable+computer+case&w4=Computer+telephony+integration&w5=Computer+telephony+integration+cti&c=5&s=151&g=2&.sig=0L45TanocmGShw91jOg7bQ>
> - Computer telephony integration<http://groups.yahoo.com/gads;_ylc=X3oDMTJjZzlkMWhhBF9TAzk3MzU5NzE0BF9wAzQEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA3NsbW9kBHN0aW1lAzExNzY3MTM5ODE-?t=ms&k=Computer+telephony+integration&w1=Computer+telephony&w2=Portable+computer&w3=Portable+computer+case&w4=Computer+telephony+integration&w5=Computer+telephony+integration+cti&c=5&s=151&g=2&.sig=q3fyEPuegir5iyfxg8W-dA>
> - Computer telephony integration cti<http://groups.yahoo.com/gads;_ylc=X3oDMTJjMWg5MGFoBF9TAzk3MzU5NzE0BF9wAzUEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA3NsbW9kBHN0aW1lAzExNzY3MTM5ODE-?t=ms&k=Computer+telephony+integration+cti&w1=Computer+telephony&w2=Portable+computer&w3=Portable+computer+case&w4=Computer+telephony+integration&w5=Computer+telephony+integration+cti&c=5&s=151&g=2&.sig=iON1CbLeehVtxqxDmeEo_A>
>
> Yahoo! Finance
>
> It's Now Personal<http://us.ard.yahoo.com/SIG=12jgb88dq/M=493064.10512181.11138666.8674578/D=groups/S=1705006764:NC/Y=YAHOO/EXP=1176721181/A=4507179/R=0/SIG=12de4rskk/*http://us.rd.yahoo.com/evt=50284/*http://finance.yahoo.com/personal-finance>
>
> Guides, news,
>
> advice & more.
> Search Ads
>
> Get new customers.<http://us.ard.yahoo.com/SIG=12isg30dt/M=493064.9803227.10510220.8674578/D=groups/S=1705006764:NC/Y=YAHOO/EXP=1176721181/A=3848641/R=0/SIG=1312g85fq/*http://searchmarketing.yahoo.com/arp/srchv2.php?o=US2003&cmp=Yahoo&ctv=Groups2&s=Y&s2=&s3=&b=50>
>
> List your web site
>
> in Yahoo! Search.
> Yahoo! Groups
>
> Start a group<http://groups.yahoo.com/start;_ylc=X3oDMTJvbWRiZDV1BF9TAzk3MzU5NzE0BF9wAzMEZ3JwSWQDMTgzOTI3NARncnBzcElkAzE3MDUwMDY3NjQEc2VjA25jbW9kBHNsawNncm91cHMyBHN0aW1lAzExNzY3MTM5ODE->
>
> in 3 easy steps.
>
> Connect with others.
> .
>
>
>
[Non-text portions of this message have been removed]
Christopher Diggins <cdiggins@...> wrote:
> The question that remains then is "why allow the compiler (or better yet,Your answer was better than mine, but I did have one little tidbit I
> the editor) infer the types instead of insisting the programmer write them
> out?".
think it worthy: a program that must be type-inferenced must be
written in a predictable manner: the compiler has to be able to figure
it out easily. This makes it generally easier to analyze even for
humans.
> Christopher Diggins-Billy
On 4/16/07, William Tanksley, Jr <wtanksleyjr@...> wrote:
>When you say "predictable" I am assuming you are referring programs
> Christopher Diggins <cdiggins@...> wrote:
> > The question that remains then is "why allow the compiler (or better yet,
> > the editor) infer the types instead of insisting the programmer write them
> > out?".
>
> Your answer was better than mine, but I did have one little tidbit I
> think it worthy: a program that must be type-inferenced must be
> written in a predictable manner: the compiler has to be able to figure
> it out easily. This makes it generally easier to analyze even for
> humans.
with straightforward or simple types, and not to the set of well-typed
programs in general.
Well I agree it would be ideal for programs to be written in a
predictable manner, I don't believe it to be a theoretical
prerequisite. I know that other type inferring compilers (e.g.
Haskell) are quite limited with regards to what they can infer but it
is mostly a combination of intention (i.e. the designers wanted a
stricter type systems than I see as being practical) and
implementation approach.
It'll remain to be seen how sophisticated the Cat inference engine
turns out to be in practice once the current version is completed. I
am confident however (based on the performance of the earlier
prototype) that Cat will be able to handle inferring the type of
complex edge-case programs with ease. This is due mainly because of
the simplicity of the type system of Cat compared to other languages.
Cheers,
Christopher
Christopher Diggins <cdiggins@...> wrote:
> William Tanksley, Jr <wtanksleyjr@...> wrote:No, I'm referring to programs with static, balanced stack effects.
> > Your answer was better than mine, but I did have one little tidbit I
> > think it worthy: a program that must be type-inferenced must be
> > written in a predictable manner: the compiler has to be able to figure
> > it out easily. This makes it generally easier to analyze even for
> > humans.
> When you say "predictable" I am assuming you are referring programs
> with straightforward or simple types, and not to the set of well-typed
> programs in general.
> It'll remain to be seen how sophisticated the Cat inference engineIn spite of what I said, I do agree that more power is better than
> turns out to be in practice once the current version is completed. I
> am confident however (based on the performance of the earlier
> prototype) that Cat will be able to handle inferring the type of
> complex edge-case programs with ease. This is due mainly because of
> the simplicity of the type system of Cat compared to other languages.
less. So go for it!
While you're at it: can you build me a type inferencer that will
distinguish the set of functions that terminate from the set of ones
that don't? ;-)
> Christopher-Billy
chris glur wrote:
> > A perhaps trivial question [which also serves to test if my - viaWilliam Tanksley, Jr wrote:
> > gmail - posts get through] is: "is it obvious why one would
> > want to 'infer the types' ?"
>
> Maybe not.OK, the old 'strongly typed vs untypes languages' debate,
>
> There are many languages that do very little typechecking at compile
> time. They include concatenative languages like Forth, Joy, and
> Postscript; people have worked with them for years. The problem is
> that many errors you can make in them are incredibly hard to narrow
> down and find, but very easy to make. You'd think that with just a
> little tiny bit of static checking you could prevent a huge, annoying
> class of problems from ever becoming an error.
>
> The problem then becomes that the programmer has to tell the compiler
> all about the types of the programs he wants to write, even though
> "types" are not what programming is supposed to be about.
>
where my prefered language is Oberon - from Wirth's
strongly typed family.
> Type Inferencing makes the compiler do a bit of work to figure outI don't like this !
> what the programmer meant, assuming that the programmer wanted to
> write a program that behaves consistently and predictably. As a bonus,
> not only does the programmer NOT have to explain all the types to the
> compiler, the programmer also gets an error from the compiler if his
> program isn't going to behave consistently and predictably.
There are 'problems' where the answers are not yet know, and where
having the machine infer is appropriate. Data 'non-typeing' is NOT
such a case. When the data is 'created' by the human's mind, the ID
and type [pair] should be specified. Then [as has been proven over
decades] type checking [not inference] should be done.
==========
Christopher Diggins wrote:
] This question implies the question "why would one want to statically verify
] the types?". This one is fairly well-known: e.g. documentation, reducing
] defects, and improving performance, so I'll assume that it is already known.
] The question that remains then is "why allow the compiler (or better yet,
] the editor) infer the types instead of insisting the programmer write them
] out?".
]
] If you want static type verification then you will encounter a fair number
] of scenarios where expressing the types is non-trivial and the type
] signature may even be longer than the function body. Sometimes the type is
] not easily deduced by a programmer due to lack of familiarity with the
] complexities of type systems, but the programmer still knows how to write
] the program they want correctly.
No, then rather write an ES to explain the 'complexities of type systems'.
How can they 'knows how to write the program they want correctly',
without knowing the types to be used ?
Similarly, smarty-pants multiple error indicating compilers are worse
than the primitive old recursive descent [eg. for pascal] which just
scrolled the source to screen, till it hit the first error.
] Finally, there are scenarios where the type
] is so trivially obvious, writing it is redundant.
]
] As for whether or not it is obvious, that really depends on your experience
] with statically typed languages, and an understanding of how the refactoring
] capabilities of modern IDEs for C# and Java actually do their magic. The
] more type inference you are able to do with a langauge, the more an IDE can
] refactor your code for you.
]
It seems intuitive that strong-typing, whether by pre-declaration or inference,
would allow better refactoring by an IDE. Smart IDE's are really what
I'd like to
know more about.
I haven't formalised yet if/why eg. lisp [and presumably joy, which I'm not
yet familiar with] can't be typed. It sure would ruin the minimalist look
and feel. With forth too, adding typing is pointless. Similarly I'm
no convinced
that infereing typing, for a language which was apparently conceived of as
being non-typed is sound ?
As typing provides extra info which can be used for checking, analagously
eg. my Oberon mail-list is better than this one, in that for any post which
I make, I get a confirming echo.
William Tanksley, Jr wrote:
> Your answer was better than mine, but I did have one little tidbit IYes, the language must be designed to catch errors by type CHECKING
> think it worthy: a program that must be type-inferenced must be
> written in a predictable manner: the compiler has to be able to
> figure it out easily. This makes it generally easier to analyze even for
> humans.
by the compiler. Indeed, work load must be removed from the
programmer; eg. by allowing whole constructs, instead of ascii-chars
being 'selected'/entered. Free up the programmer for more creative
tasks eg. selecting/designing good data names and types.
] Well I agree it would be ideal for programs to be written in a
] predictable manner, I don't believe it to be a theoretical
] prerequisite. I know that other type inferring compilers (e.g.
] Haskell) are quite limited with regards to what they can infer but it
] is mostly a combination of intention (i.e. the designers wanted a
] stricter type systems than I see as being practical) and
] implementation approach.
]
] It'll remain to be seen how sophisticated the Cat inference engine
] turns out to be in practice once the current version is completed. I
] am confident however (based on the performance of the earlier
] prototype) that Cat will be able to handle inferring the type of
] complex edge-case programs with ease. This is due mainly because of
] the simplicity of the type system of Cat compared to other languages.
OK. PS you know about a similar [infereing types] debate going on
in Newsgroups: comp.lang.functional ?
Since I don't know how gmail works [except that it seems to keep
spam out - so far] I'm going to try to just cutNpaste this to gmail
and set 'include quoted text' to No. Excuse me if I mess up.
Thanks,
== Chris Glur.
Whew, a long email.
chris glur <crglur@...> wrote:
> > The problem then becomes that the programmer has to tell the compilerAll type-inferenced languages are strongly staticly typed. If they
> > all about the types of the programs he wants to write, even though
> > "types" are not what programming is supposed to be about.
> OK, the old 'strongly typed vs untypes languages' debate,
> where my prefered language is Oberon - from Wirth's
> strongly typed family.
weren't, they wouldn't require type inferencing.
And you've misunderstood the debate. Almost no modern languages are
untyped; many of them are dynamically typed (like Python and Joy)
rather than being statically typed (like Oberon).
Most of the currently existing concatenative languages are dynamically
typed; Factor can express some types, and may optionally enforce them
(I don't know). Enchilada is actually untyped, and thus qualifies as a
"rare bird" (it has only one type that can serve as any kind of data).
Forth has types, but doesn't enforce them at all. Cat and strongForth
are the only concatenative languages I know of that consistently
statically enforce types.
(I agree that Oberon is a pretty cool language, by the way.)
> > Type Inferencing makes the compiler do a bit of work to figure outIf the answers are unknown, having the machine infer them is
> > what the programmer meant, assuming that the programmer wanted to
> > write a program that behaves consistently and predictably. As a bonus,
> > not only does the programmer NOT have to explain all the types to the
> > compiler, the programmer also gets an error from the compiler if his
> > program isn't going to behave consistently and predictably.
> I don't like this !
> There are 'problems' where the answers are not yet know, and where
> having the machine infer is appropriate.
_impossible_. Type inference is only possible in the simple cases --
in general it's an NP complete problem.
> Data 'non-typeing' is NOTThis is a non-sequitur. We're not talking about untyped data; we're
> such a case. When the data is 'created' by the human's mind, the ID
> and type [pair] should be specified.
talking about statically typed data. When the data is created, the
type is always specified; but when a function is written that can
apply to only one type, why should you have to explain which type it
is?
> Then [as has been proven over decades] type checking [not inference]Why not both?
> should be done.
> ==========Christopher's answer was better than mine; his question (which I've
> Christopher Diggins wrote:
> ] The question that remains then is "why allow the compiler (or better yet,
> ] the editor) infer the types instead of insisting the programmer write them
> ] out?".
quoted above) gets right to the issue.
By the way, the ONLY thing type inference replaces is having the
programmer write out the type signatures of functions. It doesn't
replace data types, and doesn't make it possible to write type-unsafe
code; in fact, generally it makes it harder, since you have to write
code that that computer can prove is safe.
> ] If you want static type verification then you will encounter a fair numberWhat does "ES" mean?
> ] of scenarios where expressing the types is non-trivial and the type
> ] signature may even be longer than the function body. Sometimes the type is
> ] not easily deduced by a programmer due to lack of familiarity with the
> ] complexities of type systems, but the programmer still knows how to write
> ] the program they want correctly.
> No, then rather write an ES to explain the 'complexities of type systems'.
> How can they 'knows how to write the program they want correctly',Of course they know the types to be used. But properly specifying the
> without knowing the types to be used ?
types can be very difficult and lengthly. You don't have much
experience with strong static typechecking systems, since you're only
used to Oberon, but in a system that actually enforces types you can't
insert an item into a list unless the type of the list allows that
type of item insertion (Oberon allows any object to be inserted into
any list); and functions may only be called in locations where their
types allow such a call. Specifying those things for every place
they're used can become exhausting.
> ] Finally, there are scenarios where the typeThis is a surprisingly big win for type inference :-).
> ] is so trivially obvious, writing it is redundant.
> ] As for whether or not it is obvious, that really depends on your experienceAgreed.
> ] with statically typed languages, and an understanding of how the refactoring
> ] capabilities of modern IDEs for C# and Java actually do their magic. The
> ] more type inference you are able to do with a langauge, the more an IDE can
> ] refactor your code for you.
> It seems intuitive that strong-typing, whether by pre-declaration or inference,
> would allow better refactoring by an IDE. Smart IDE's are really what
> I'd like to know more about.
I'd like to hear more about what you're thinking of in the area of
IDEs. I've done a little thinking about them, and of course I use a
moderately smart one at work (Eclipse), but there's plenty more to do.
The only real idea I've had for a smart IDE for a concatenative
language would be an IDE that, when you hovered the cursor on a word,
would draw graphical arrows showing where the word's data came from.
Refactoring support is wonderful, but would depend on the specific
language -- in general, Extract Method is simple in a concatenative
language :-), so presumably other refactorings would be more useful.
(Of course, it's trivial in a flat language -- but since there are no
practical flat languages yet we'll just have to wait.)
> I haven't formalised yet if/why eg. lisp [and presumably joy, which I'm notCommon Lisp does not have a minimalist look and feel :-). Static
> yet familiar with] can't be typed. It sure would ruin the minimalist look
> and feel.
typechecking for Common Lisp has been done -- the language includes
all the type specifiers, so all you have to do is tell the compiler to
look for them.
Joy probably won't be typechecked, but Cat could be said to be Joy's
descendant, and it certainly is.
> With forth too, adding typing is pointless.I'm not sure why you'd say that, but even if it's true, someone did it
:-). StrongForth is available under the GPL at
http://home.vrweb.de/stephan.becher/forth/. The author originally
created the static typechecking and subtype polymorphism algorithm to
help him manage all the different types of addresses he had to work
with in a particular embedded processor.
There's no reason why the algorithm would only work on Forth; it's
quite general and very simple. The full StrongForth implementation is
fairly complex, but that's because it attempts to imitate ANSI Forth,
which is not designed for strong static typechecking.
> Similarly I'm no convincedThat's why Cat was designed from the ground up to be type inferenced.
> that infereing typing, for a language which was apparently conceived of as
> being non-typed is sound ?
Factor wasn't, but I would expect that it would work well; the author
is not known for sloppiness.
> As typing provides extra info which can be used for checking, analagouslyGenerally speaking, inference is stricter than explicit specification.
With inference, the program alone must be unambiguous about what it's
doing; with explicit specification, it can be vague.
> OK. PS you know about a similar [infereing types] debate going onNot in the sense of seeing it, but I've been in that newsgroup before,
> in Newsgroups: comp.lang.functional ?
and I have faith that particular discussion is still alive and well.
It's been running for years now -- perhaps not under the title it has
now, but certainly the same basic discussion, hitting the same basic
points.
There's nothing to debate; a statically typed language with type
inferencing is better that a statically typed language without, UNLESS
the language has to be interpreted faster than the type inferencer
will run. But if that's the case, it's usually more sensible to do
dynamic type checking.
> == Chris Glur.-Billy
William Tanksley, Jr scripsit:
> By the way, the ONLY thing type inference replaces is having theMost type-inferencing languages allow a modicum of explicit typing in
> programmer write out the type signatures of functions. It doesn't
> replace data types, and doesn't make it possible to write type-unsafe
> code; in fact, generally it makes it harder, since you have to write
> code that that computer can prove is safe.
the situation where the compiler cannot decide: for example, you cannot
write "double x = x + x" in Standard ML, because the compiler cannot
decide if x is floating-point or integer, so you must use an explicit type.
> > It seems intuitive that strong-typing, whether by pre-declaration or inference,In fact, the whole concept and technology of refactoring arose in the
> > would allow better refactoring by an IDE. Smart IDE's are really what
> > I'd like to know more about.
>
> Agreed.
Smalltalk community, using a language that has always been dynamically
typed.
--
John Cowan http://ccil.org/~cowan cowan@...
Lope de Vega: "It wonders me I can speak at all. Some caitiff rogue did
rudely yerk me on the knob, wherefrom my wits still wander."
An Englishman: "Ay, a filchman to the nab betimes 'll leave a man
crank for a spell." --Harry Turtledove, Ruled Britannia