Home » forums » Site Discussion

Looking for Classic Types Thread

hi,

my google-fu is failing me. there's a discussion from way back where frank discusses what types are with someone who, maybe incorrectly, i think is involved with game design. this other person argued type theory was based on sets (i can't remember the full argument), frank that category theory was a better approach.

i realise that this could describe an awful lot of discussions, but this was a particularly detailed exchange and it was fairly early on in the site's history.

does this ring bells with anyone else? any pointers? thanks.

By andrew cooke at 2004-09-16 22:14 | Site Discussion | previous forum topic | next forum topic | other blogs | 10071 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Probably one of these discussions

Python Metaclass Programming

Hundred Year Language

My google-fu kata was this (without quotes): "Tim Sweeney Frank Atanassow Category Theory Set Type site:lambda-the-ultimate.org".

By Daniel Yokomizo at Fri, 2004-09-17 00:23 | login or register to post comments

brilliant. it was the python

brilliant. it was the python thread. i kept finding the 100 year language one with google, but not the python one. thanks! (and apologies tim, for forgetting your name - when i saw it in the 100 year language thread i thought "no, it was someone else" for some reason).

By andrew cooke at Fri, 2004-09-17 00:34 | login or register to post comments

More On Types :-)

Relax, I'm not re-opening the "what are types?" debate. I only wish to point out that I don't recall that Tim went so far as to claim that "type theory is based on set theory," but rather only that there is a particular language, David McAllester's Ontic, that takes a "types as sets of potential values" stance, where "potential values" are literally defined in terms of nondeterministic enumeration. I suppose there's a question as to whether that's "expressive enough" for purposes that you care about (although Ontic has slightly more expressive power than Zermelo-Fränkel with the Axiom of Choice, so it seems that "lack of expressive power" would be a tough argument to make).

In fairness to Frank, I believe he knows all of this, and was making the larger point that while Ontic's choices might be a nice way to implement a kind of dependent type system, he's not convinced that dependent types are desirable, and there are good Category Theoretic reasons for such skepticism.

Of course, I could be reading them both completely wrong. :-)

By Paul Snively at Fri, 2004-09-17 00:54 | login or register to post comments

What's the color of a two-cent piece? Copper, copper...

Actually my position now is that dependent types are desirable for composing homogeneous implementations of things (because you can assert via type equality that two ADT's have the same representation), but that what one wants to do more often is to compose heterogeneous implementations of things (where the representations are less than equal, like say isomorphic). The reason for that is that there are so many choices of representation available even for trivial ADTs; forcing them to be compatible at the level of of equality requires a major coincidence, a performance hit, or a global policy to which all library writers must adhere to.

I don't think one needs to make a choice between dependent types and a mechanism supporting what I want; I just think dependent types would not be as valuable in practice.

By Frank Atanassow at Fri, 2004-09-17 18:38 | login or register to post comments

Is an implementation on the way?

I was curious to know if you are on the way to implementing what you were talking about in the metaclasses thread.
or have you already addressed this elsewhere?

By Jeff Cutsinger at Wed, 2004-09-22 16:16 | login or register to post comments

Academia: City of Saints and Madmen

I have not implemented it because I am still struggling to nail down the formal definition and semantics. That will go in my thesis, and will be submitted next month as an article to an academic conference (or so I hope—last time I mentioned it I said this month...). Then I might implement it; it won't be a full-blown language, since I expect adding general recursion and whatnot will pose its own problems. (Then again, it might be easy to do it in a suboptimal way.) My next job will probably revolve mostly around making the language more practical.

Since my thesis and continued career as an academic hinge on this, though, you can rest assured it will get done. Either that, or I will slink into a dark corner and you will never hear from me again. :)

By Frank Atanassow at Thu, 2004-09-23 18:39 | login or register to post comments