> > Lennart Augustsson <[EMAIL PROTECTED]> wrote: <snip>
> Jonathan Cast wrote: > > > > Here is (approximately) the Core translation of foo above: > > > > > >>foo :: forall a b. Either a b -> Either () b > >>foo = /\ a b -> \ e -> case e of > >> Left _ -> Left @() @b () > >> Right _ -> e > > > > > > You call this as (foo @a @b e), where e has type (Either a b). > > > > So, the call (foo @a @b (Right @a @b x)) reduces (ignoring types) to > > (Right @a @b x). This reduces a term of type (Either () b) to one > > of type (Either a b). That's not type safe. > > There are no types around at run time We agree on this, but disagree on the reason. I think we may have to agree to disagree on the reason, but I would rather explain my position first (see below). > so in case foo is being passed a Right argument the representation of > the result is identical to the argument. So? Types are logical tools we use to structure our programs and guarantee their safety; type safe is a sufficient condition for ``will not segfault (or similarly fail)'', not an equivalent condition. In any case, it doesn't matter. If I say: > newtype Plus alpha beta = Plus (Either alpha beta) > bat :: Plus alpha beta -> Either alpha beta > bar x = x bar's result is /guaranteed/ by the standard to have the same representation as its argument, but it still doesn't type check. Why? Because ``type safe'' doesn't mean ``uses the right representation at run time''. Types are not a computer science concept; they are a foundation of mathematics concept, invented around the turn of the previous century I believe by Bertrand Russell to get around certain logical problems in set theory, and I believe brought to prominence by Martin-Löf as a foundation for intuitionistic mathematics. Types made their first contact with lambda-terms in Alonzo Church's time, at which point the lambda-calculus was still intended as a system for foundations of mathematics. We use types in computer science because they are useful, but they don't arise from information theory or representation theory or any other branch of computer science. Therefore, genuine types don't exist at run time. In any language. Types are not properties of programs (which are not mathematical objects), but rather of languages (which are); since no machine language (that I know of) is typed, types do not exist at run time. No type theory (that I know of) goes beyond System F in accepting anything like foo. So, given the current state of the art, foo is unconditionally ill-typed. That could change if someone comes up with a /consistent/ type theory that accepts foo, but foo is ill-typed at the moment. > (OK, if you want to be very pedantic, this isn't necessarily true for > every possible implementation of Haskell, just all existing ones. :) ``Perfectly correct'' is an open invitation to pedanticism :) Jon Cast _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe