# Cat Type Inference

## Christopher Diggins — 2007-04-11 19:10:35

    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 — 2007-04-16 08:59:38

    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

    >

## William Tanksley, Jr — 2007-04-16 14:00:01

    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' ?"

     Maybe not.

    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

## Christopher Diggins — 2007-04-16 16:31:08

    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]

## William Tanksley, Jr — 2007-04-16 18:07:37

    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.

     > Christopher Diggins

     -Billy

## Christopher Diggins — 2007-04-16 19:20:21

    On 4/16/07, William Tanksley, Jr <wtanksleyjr@...> wrote:

     >

    > 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.

     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.

    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

## William Tanksley, Jr — 2007-04-16 19:55:39

    Christopher Diggins <cdiggins@...> wrote:

     > William Tanksley, Jr <wtanksleyjr@...> wrote:

    > > 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.

     No, I'm referring to programs with static, balanced stack effects.

     > 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.

     In spite of what I said, I do agree that more power is better than

    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 — 2007-04-17 15:17:09

    chris glur  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' ?"

    >

     William Tanksley, Jr wrote:

     > Maybe not.

    >

    > 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.

    >

     OK, the old 'strongly typed vs untypes languages' debate,

    where my prefered language is Oberon - from Wirth's

    strongly typed family.

     > 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.

     I don't like this !

    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 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.

     Yes, the language must be designed to catch errors by type CHECKING

    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.

## William Tanksley, Jr — 2007-04-17 17:45:09

    Whew, a long email.

    chris glur <crglur@...> wrote:

     > > 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.

    > OK, the old 'strongly typed vs untypes languages' debate,

    > where my prefered language is Oberon - from Wirth's

    > strongly typed family.

     All type-inferenced languages are strongly staticly typed. If they

    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 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.

    > I don't like this !

    > There are 'problems' where the answers are not yet know, and where

    > having the machine infer is appropriate.

     If the answers are unknown, having the machine infer them is

    _impossible_. Type inference is only possible in the simple cases --

    in general it's an NP complete problem.

     > 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.

     This is a non-sequitur. We're not talking about untyped data; we're

    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]

    > should be done.

     Why not both?

     > ==========

    > 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?".

     Christopher's answer was better than mine; his question (which I've

    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 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'.

     What does "ES" mean?

     > How can they 'knows how to write the program they want correctly',

    > without knowing the types to be used ?

     Of course they know the types to be used. But properly specifying the

    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 type

    > ] is so trivially obvious, writing it is redundant.

     This is a surprisingly big win for type inference :-).

     > ] 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.

     Agreed.

    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 not

    > yet familiar with] can't be typed. It sure would ruin the minimalist look

    > and feel.

     Common Lisp does not have a minimalist look and feel :-). Static

    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 convinced

    > that infereing typing, for a language which was apparently conceived of as

    > being non-typed is sound ?

     That's why Cat was designed from the ground up to be type inferenced.

    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, analagously

     Generally 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 on

    > in Newsgroups: comp.lang.functional ?

     Not in the sense of seeing it, but I've been in that newsgroup before,

    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

## John Cowan — 2007-04-17 18:54:18

    William Tanksley, Jr scripsit:

     > 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.

     Most type-inferencing languages allow a modicum of explicit typing in

    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,

    > > would allow better refactoring by an IDE. Smart IDE's are really what

    > > I'd like to know more about.

    >

    > Agreed.

     In fact, the whole concept and technology of refactoring arose in the

    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