The Artima Developer Community
Sponsored Link

Weblogs Forum
Online Programming Lanugage Discussions

4 replies on 1 page. Most recent reply: Sep 7, 2006 11:33 PM by Cleo Saulnier

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 4 replies on 1 page
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Online Programming Lanugage Discussions (View in Weblogs)
Posted: Sep 3, 2006 4:08 PM
Reply to this message Reply
Summary
I haven't been posting as much at Artima lately, but I have been posting a fair amount of questions and ideas at Lambda-the-Ultimate.org.
Advertisement
I know that some of the readers of my blog are particularly interested in my blog posts about language design, but unfortunately I haven't been making as many contributions lately. The truth is that I have been wrestling with some pretty significant bugbears with regards to the Cat type system. To help defeat them, I have been calling on the big guns at Lambda-the-Ultimate.org, a discussion site for programming language and type system theorists.

Lambda-the-Ultimate.org is admittedly over my head at times, but sometimes jumping into the deep end is the best way to learn to swim. It is a good place to hang out for aspiring language designers. They do have their own jargon at that site which can be a bit impenetrable at times, so I recently purchased the Types and Programming Languages book by Benjamin C. Pierce.

What is happening right now with Cat is that I am trying to merge static type-checking and dynamic type-checking in a single language. Not really anything new when you think about it. many languages support or at least provide the tools to implement variant types. What I am doing a bit different is that types have become first class values in Cat, and the core language is dynamically typed. At the same time Cat supports, and in fact encourages, type annotations, and optional compilation.

If a Cat program is compiled then the compiler is expected to precompute the type-expressions the same way compilers for other language precompute constant integer expressions. Like how 2 + 5 will often be replaced with the value 7 at compile-time.

In language implementation news, the newest version of Cat is approaching completion, but I want to finish some more of the type checking functionality first before I put it out there.


Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Online Programming Lanugage Discussions Posted: Sep 5, 2006 7:20 AM
Reply to this message Reply
> To help defeat them, I
> have been calling on the big guns at <b><a
> href="http://lambda-the-ultimate.org/user/1261/track">Lambd
> a-the-Ultimate.org</a></b>, a discussion site for
> programming language and type system theorists.

There's certainly a lot of very bright people, there. I've recently bought several books on computer science/programming language therory and type theory, myself, including the one you mention in your blog (as well as some maths books - such as books on lambda calculus and category theory), to be able to actually understand what they talk about in such discussions, and be able to participate. :)

The books I've bought (on programming languages and types), are:

- "Concepts, Techniques, and Models of Computer Programming"
- "Types and Programming Languages"
- "Advanced Topics in Types and Programming Languages"

However, I've not got around to read these, yet. It seems I'll have enough to read for a while. :)

Some maths books on interesting, and computer science-relevant topics, that I've also recently bought (which I haven't read, either):

- "Conceptual Mathematics: A First Introduction to Categories"
- "Basic Category Theory for Computer Scientists"
- "An Introduction to Lambda Calculi for Computer Scientists"
- "Introduction to Topology"
- "A Combinatorial Introduction to Topology"
- "Algebraic Topology"

I typically buy several books on topics, as they tend to complement each other, and it gives a better chance of getting one or a few that are really good. :)

> It is a good place to hang out for aspiring language designers.

Definitely. I was reading a very interesting thread there a few days ago: "Why type systems are interesting" (http://lambda-the-ultimate.org/node/100), and was thinking: "This is something Christopher Diggins should read" (I assumed it could be of interest to you, from knowing your interest in programming language design and type systems), but I see you're already well familiar with the site. :)

> What is happening right now with Cat is that I am trying
> to merge static type-checking and dynamic type-checking in
> a single language.

As you've seen from the thread you linked to, "dynamic typing" isn't really a term that is well accepted by type theorists, as they instead prefer to call dynamically typed languages "untyped languages"... :)

From http://en.wikipedia.org/wiki/Type_theory:

"Definitions of type system vary, but the following one due to Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:

[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
(Pierce, 2002)"

In other words, the term "dynamic typing" appears to be something of a contradiction, in terms of classical type theory. Using the above conventional definition of "type", "dynamically typed languages" are basically "untyped" - all variables are of a "universal type" (variant).

Terje Slettebø

Posts: 205
Nickname: tslettebo
Registered: Jun, 2004

Re: Online Programming Lanugage Discussions Posted: Sep 5, 2006 7:52 AM
Reply to this message Reply
Just to add (from: http://lambda-the-ultimate.org/node/100#comment-1018):

"In that context, what we call "types" in dynamic languages can't really be considered types, so they're called tags instead."

However, he also adds:

"Naturally, all sorts of terminological shenanigans ensue, because of course the things that type theorists don't want to call types are, to a first approximation at least, actually the dynamic equivalent of the static entities they do call types."

Todd Blanchard

Posts: 316
Nickname: tblanchard
Registered: May, 2003

Re: Online Programming Lanugage Discussions Posted: Sep 5, 2006 7:08 PM
Reply to this message Reply
You might look at Strongtalk. It was proceeding along these lines.

Some links:
http://bracha.org/nwst.html
http://strongtalk.org/index.html
http://lambda-the-ultimate.org/classic/message4826.html

Cleo Saulnier

Posts: 77
Nickname: vorlath
Registered: Dec, 2005

Re: Online Programming Lanugage Discussions Posted: Sep 7, 2006 11:33 PM
Reply to this message Reply
They don't like me over at lambda. They're all functional freaks. The fact that the site is called 'lambda' should have been a clue. Take my advice, don't go in there claiming that functional programming is the single worst thing to hit the programming field which set it back 1000 years. Although I can support my argument, they're not interested in hearing about it. So expect a lot of closed-mindedness and don't go in guns blazing.

BTW, does a type contain everything needed to create its instance (other than the value(s) of course) or does an instance know its type? What contains what in your Cat language? Hope my question made sense. Thanks!

Flat View: This topic has 4 replies on 1 page
Topic: Online Programming Lanugage Discussions Previous Topic   Next Topic Topic: Netbeans Module for JMX enabling your application


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us