The Artima Developer Community
Articles | News | Weblogs | Books | Forums
Artima Forums | Articles | Weblogs | Java Answers | News
Sponsored Link •

Weblogs Forum
Type Inference is Good

6 replies on 1 page. Most recent reply: Oct 4, 2006 8:05 AM by Alex Stojan

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 6 replies on 1 page
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Type Inference is Good (View in Weblogs)
 		Posted: Sep 29, 2006 10:45 PM
Reply to this message Reply
Summary
Wherein I talk about the merits of type inference, the latest Cat release, unit tests, and miniature computers.
Advertisement
I just posted a considerably more stable version of Cat (version 0.7.1) online at http://www.cat-language.com which has a working type inference engine for both stacks (previously it only sort-of worked for trivial expressions on a single stack).

I have been retroactively adding unit tests. (I can already hear Michael Feathers saying "You should have been writing the tests first!"). While I am a proponent of test driven development (TDD) in theory, to be completely candid I didn't actually practice it. Now that I am developing in C#, I find it easier for some reason (perhaps less fear of writing in an OOP style ... the C++ community frowns on OO style code for some reason?!). Writing a type inference engine is of sufficient complexity that I found that I I didn't have much choice: write unit tests or give up. Adding unit tests even this late in the game was still a great idea! I managed to work out a lot of kinks very quickly (much more so than external test suites). It also has been forcing me to remove unneccessary coupling in the code base.

Not many languages support type inference, but it is very useful. In fact it is indispensible in to have type inference in a language like Cat which has a strong type system. In Cat there are two stacks, and every operation is a transition from these two stacks to two other stacks. As a result type notation looks like: 

define add_and_load : (int int)()->()(int) { add_int load }
Clearly it is a bit silly if your language requires more complexity to express types than the actual code! Now in Cat you can write: 
define add_and_load { add_int load }
and the interpreter will figure out the type for you. You can ask for the type explicitly using: 
@add_and_load type_of
This is in fact only the tip of the iceberg. Cat types can quickly get quite very sophisticated because it supports polymorphism (the C++ kind, not the ML kind ... what is it called universal quantification or something?).

The type of the Cat if operation is rather involved: 

define if : (bool (A)->(B) (A:any*)->(B:any*))->(B)
Here is what this means in English: the if operation requires two functions of the same type on the top of the stack, and below that a boolean value. If the value is false, then the first function popped off the stack is executed, otherwise the other one is executed.

So this might seem like nothing fancy on the surface but consider the following: the MSIL (Microsoft Intermediate Language) byte-code has a similar restriction on "if" assembly code instructions. It is just that in Cat this is expressed naturally using a type-system.

This is almost precisely why I invented Cat: it maps to and from assembly code and while maintaining a strong type system. It also cleanly maps to and from other imperative languages (like Heron ... see where I am going with this?). Of course Cat can do a lot of things most assembly code can only dream of.

I have a lot of possible applications in mind for Cat, and something while pulls at my heart is as a language for developing applications on the latest generation of miniature and cheap computers (http://linuxdevices.com/news/NS6828123924.html and http://laptop.org/).


Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Type Inference is Good Posted: Oct 2, 2006 3:32 AM
Reply to this message Reply
> Now that I am
> developing in C#, I find it easier for some reason
> (perhaps less fear of writing in an OOP style ... the C++
> community frowns on OO style code for some reason?!).

I think it would be more correct to say that they frown at _inappropriate_/unnecessary use of OO, such as using a member function for something that might be better done with a free function.

Take std::string, as an exmaple: Its design is widely derided, even in the community, itself, for its bloated interface. As Kevlin Henney said it: "If std::string looks like it was designed by a committee, it's because it was." :)

Instead, you might have a few core functions - those that are needed to maintain invariants, and leaving the rest (like searching, sorting, etc.) as free functions. There's a very good article about this here: "The C++ Style Sweet Spot" (http://www.artima.com/intv/goldilocks.html)

Unfortunately, mixing member functions and non-member functions lead to two different calling conventions, in C++, but it doesn't have to be like that.

Java programmers typically overuse OO, when going to C++ (I did it as well, having done Java for a while, and coming back to C++ several years ago), as there's for example no free functions in Java. The "static import" stuff that has been added more recently might be used to work around that, though.

> This is in fact only the tip of the iceberg. Cat types can
> quickly get quite very sophisticated because it supports
> polymorphism (the C++ kind, not the ML kind ... what is it
> called universal quantification or something?).

I'm not sure what you're thinking of, and was it the C++ kind or the ML kind you were looking for the name of? Also, from the cat examples, I'm not sure which corresponding C++ polymorphism you were thinking of (if it wasn't ML), but anyway, one term for the inheritance-and-virtual-functions polymorphism is "inclusion polymorphism" (because the type used has to be included in the hierarchy), whereas templates/generics go by the name of "parametric polymorphism"/"unbounded polymorphism".

I guess you might be thinking of templates, as they essentially model the mathematical expression "for all T..." (http://en.wikipedia.org/wiki/Universal_quantification)

Concepts/type classes would then be a way to say "For all T where..." :)

I don't have much experience with type inference, myself (note that C++ will get more of this in the next version of the standard, with "auto"/"decltype"), but I'd like to become more familiar with Haskell/ML.

> <pre>
> define if : (bool (A)->(B) (A:any*)->(B:any*))->(B)
> </pre>
>
> Here is what this means in English: the if operation
> requires two functions of the same type on the top of the
> stack, and below that a boolean value. If the value is
> false, then the first function popped off the stack is
> executed, otherwise the other one is executed.

Interesting. It looks like a dependent type system. :)

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Type Inference is Good Posted: Oct 2, 2006 8:15 PM
Reply to this message Reply
> I'm not sure what you're thinking of, and was it the C++
> kind or the ML kind you were looking for the name of?
> Also, from the cat examples, I'm not sure which
> corresponding C++ polymorphism you were thinking of (if it
> wasn't ML), but anyway, one term for the
> inheritance-and-virtual-functions polymorphism is
> "inclusion polymorphism" (because the type used has to be
> included in the hierarchy), whereas templates/generics go
> by the name of "parametric polymorphism"/"unbounded
> polymorphism".
>
> I guess you might be thinking of templates, as they
> essentially model the mathematical expression "for all
> T..."
> (http://en.wikipedia.org/wiki/Universal_quantification)

I thought C++ templates don't fully model universal quantification. Consider the following:

<pre>
template&lt;typename T>
T double(T x)
{
return x + x;
}
</pre>

The only values for T which are valid are those which support addition.

Thanks for reminding me of the terms I was looking for.

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Type Inference is Good Posted: Oct 3, 2006 2:59 AM
Reply to this message Reply
> > I guess you might be thinking of templates, as they
> > essentially model the mathematical expression "for all
> > T..."
> > (http://en.wikipedia.org/wiki/Universal_quantification)
>
> I thought C++ templates don't fully model universal
> quantification. Consider the following:
>
> template<typename T>
> T double(T x)
> {
> return x + x;
> }
>
> The only values for T which are valid are those which
> support addition.

Naturally. Only the function template signature model universal quantification; what happens in the body depends on the properties of the types. It's this mismatch that "concepts" are meant to address:

template<Addable T>
T double(T x)
{
return x + x;
}

We then get something like "For all T where "T+T" yields a value of type T..."

Alex Stojan

Posts: 95
Nickname: alexstojan
Registered: Jun, 2005

Re: Type Inference is Good Posted: Oct 3, 2006 7:28 AM
Reply to this message Reply
> Naturally. Only the function template signature model
> universal quantification; what happens in the body depends
> on the properties of the types. It's this mismatch that
> "concepts" are meant to address:
>
> template<Addable T>
> T double(T x)
> {
> return x + x;
> }
>
> We then get something like "For all T where "T+T" yields a
> value of type T..."

I think with Concepts we can write something like:

concept Addable<typename T> {
T x, y;
x + y;
}

and then use it:

template<typename T> where Addable<T>
T double(T x) {
return x + x;
}

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Type Inference is Good Posted: Oct 4, 2006 1:28 AM
Reply to this message Reply
> > Naturally. Only the function template signature model
> > universal quantification; what happens in the body
> depends
> > on the properties of the types. It's this mismatch that
> > "concepts" are meant to address:
> >
> > template<Addable T>
> > T double(T x)
> > {
> > return x + x;
> > }
> >
> > We then get something like "For all T where "T+T" yields
> a
> > value of type T..."
>
> I think with Concepts we can write something like:
>
> concept Addable<typename T> {
> T x, y;
> x + y;
> }
>
> and then use it:
>
> template<typename T> where Addable<T>
> T double(T x) {
> return x + x;
> }

Yes, but with the current proposal (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2042.pdf), you can also use the "shorthand" syntax I used:

template<Addable T>
T double(T x)
{
return x + x;
}

Moreover, in the original two proposals, one of them had "usage based" concept specification, like you show here in your concept definition. However, in the subsequent joint proposal, they've gone for the other alternative, "pseudu signatures", so the concept might now be written as:

concept Addable<typename T>
{
T operator+(const T &);
}

Alex Stojan

Posts: 95
Nickname: alexstojan
Registered: Jun, 2005

Re: Type Inference is Good Posted: Oct 4, 2006 8:05 AM
Reply to this message Reply
>
> Yes, but with the current proposal
> (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2
> 042.pdf), you can also use the "shorthand" syntax I used:
>
> template<Addable T>
> T double(T x)
> {
> return x + x;
> }
>
> Moreover, in the original two proposals, one of them had
> "usage based" concept specification, like you show here in
> your concept definition. However, in the subsequent joint
> proposal, they've gone for the other alternative, "pseudu
> signatures", so the concept might now be written as:
>
> concept Addable<typename T>
> {
> T operator+(const T &);
> }

Thanks for the link! I wasn't aware of the alternative proposal.

Flat View: This topic has 6 replies on 1 page
Topic: Type Inference is Good Previous Topic   Next Topic Topic: The JVM as an (Un)Common Language Runtime
Sponsored Links


Google
  Web Artima.com   

Copyright © 1996-2019 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use