[Haskell-cafe] type inference and named fields
Jonathan Cast
jcast at ou.edu
Fri Jun 24 09:57:20 EDT 2005
> > Lennart Augustsson <lennart at augustsson.net> 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
More information about the Haskell-Cafe
mailing list