[Haskell-cafe] type inference and named fields

[Jonathan Cast]

> > 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