On 29 August 2013 05:03, Jonathan S. Shapiro <[email protected]> wrote:
> E's reply messages are first class and dynamically typed. In consequence,
> the E "WHEN" clause cannot be described in a conventional static type
> system. It might be possible to do it in a dependent type system, but it's
> not clear that the resulting check has any practical utility.

Well, the conclusion doesn't follow, but your point about utility is
appropriate, so I'll address that below.

Sandro: see, the problem is with different values of T. I can solve
this problem a few ways, and in a language without style perhaps
neither feels particularly uncomfortable.  To use the vet example, I
could have

when (farDog, resDog => { // farDog : Ref Dog
  when (farCar, resCar => { // farCar : Ref Car
    resCar.driveTo(vet, resDog);
  });
});

Or I could correctly type a two-argument form

public static void when<T0, T1>( Ref T0, Ref T1, (T0, T1) => Void );

Now yes, I can expect the body to accept an array of untyped Refs.
And because we can do RTTI, I can make use of them, albeit with some
syntactic overhead.  But once we introduce unboxed types everywhere,
casting back to the correct ref type is no longer possible.


So, to utility (:

I just really think that a systems language is where you end up doing
this sort of plumbing a lot - you're reflecting FFI function types,
you're writing linkers and GCs that operate on the program they are
actually a component of, you're emitting specialised calls in your
parser generator.  Or maybe you're deriving show on a pure datatype -
it basically involves doing the same thing, because iterating over
tags or tuple items in a safe manner is very similar to iterating over
the arguments of a function type or generating an argument list and
applying the function to it.  I wouldn't want to be using reflection
heavily for that, I'd rather have the type system ensure that I've got
the appropriate evidence of the validity of the operation.

All the standard arguments for row polymorphism apply, but unboxed
types change your ability to use existing mechanisms.

I just feel that a safe language without that sort of flexibility in
the type system will mean people are still dropping down into ASM or C
to get things done, and relying heavily on dynamic checks and
reflection otherwise.

-- 
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law.  You absolutely may reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in.  Any attempt to deny you those rights would be illegal without
prior contractual agreement.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to