master caster

[tiedyedave]

From Pierce's Types and Programming Languages:

"There are three rules for type casts: in an upcast the subject is a subclass of the target, in a downcast the target is a subclass of the subject, and in a stupid cast the target is unrelated to the subject."

Comments

[rjmccall.livejournal.com]

To the Honored Fathermaster David Wilson Kitchin IV:

Suppose a functional language were to replace concrete types with signatures, so that "int" would simply be a signature with a standard presumed implementation using machine integers. Is there any use for subtyping in such a language?

I also wonder how such a language might express tagged sums (which would presumably still be useful for structure implementation)?

Your disciplined discipline,
J.

[mtolan.livejournal.com]

That, sir, is a poor defintion.
One could characterize all stupid casts in java as an upcast to java.lang.Object, followed by a the relevant downcast. This would make it possible to eliminate all stupid casts in java, which is clearly a contradiction.
Proof by Contradiction.

special guest replier!

[adamch.livejournal.com]

You can encode Everything in untyped lambda calculus, and so you can encode Everything with "objects" where each has one method (an 'apply' method). The idea is to encode any object as a function analogous to an elimination rule of a type system. So, for example, a sum can be represented as a function that takes two arguments. Each is a function that takes the value carried by one of the branches of the sum and does what it pleases with it. The value for the sum runs its first argument if it inhabits the left branch and its second argument if it inhabits the right branch.

As for the use of subtyping, I personally wouldn't want to have it, but there are standard treatments of subtyping for lambda calculus.

[rjmccall.livejournal.com]

Nope. No amount of object casting will make, say, (float) ThomasPyncheon any less stupid.

Re: special guest replier!

[rjmccall.livejournal.com]

I, too, have studied lambda calculus in the past; the challenge was not to embed sum types in the implementation (which would probably not run on the untyped lambda calculus) but to find an adequate signaturing mechanism for sum types, such that they could still be computably case-analyzed.

Re: special guest replier!

[adamch.livejournal.com]

For the type (T + U), the signature can be:

method case : forall V, (T -> V) -> (U -> V) -> V

[ikeepaleopard]

IEEE Thomas Pynchon, author of The Crying of Lot 49.00000001247?

[rjmccall.livejournal.com]

"d(God,Chance)< 2^-149"
-- IEEE Thomas Pynchon

Re: special guest replier!

[rjmccall.livejournal.com]

That's not bad; I hadn't considered making case part of the signature, but it's clearly the sensible move. Maybe a record type instead of a curried list, since ordering is a bit arbitrary -- so, in SML syntax:

datatype foo = bar of X | baz of Y
val case: { bar: X -> 'a, baz: Y -> 'a } -> foo -> 'a

[gustavolacerda.livejournal.com]

Thanks for reminding me! I just reached and grabbed this book without getting up from my chair. Which I really should do, since I'm finally doing a class on type theory, lambda calculus, etc.. and now I guess I have a better chance of understanding it.

[tiedyedave]

Who are you, anyway? I don't mind at all if you friended me out of the blue due to common interest or curiosity, but I just want to make sure that you aren't someone I've actually met and subsequently forgotten (though this seems unlikely given that you're in Amsterdam).

Regardless of the answer to the above, I am impressed that {cognitive science, functional programming, libertarianism, taoism} are all in the intersection of our interests.

[gustavolacerda.livejournal.com]

Indeed, we never met, AFAIK.