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.
On Tue, Aug 27, 2013 at 9:55 PM, William ML Leslie < [email protected]> wrote: > I would like to correctly type E's `when` operator in any given > language. That is, given a delegate taking refs (Ref T0, Ref T1, .. > Ref Tn) returning Void, and an appropriate rest argument of refs, let > me apply the delegate. (using * rather than ... to denote varargs > here but the rest should be straightforward, omitting things like > broken ref handling) > > when : {argtypes : Vec n ({t} -> Ref t)} -> (f : argtypes -> ()) -> > (args : *argtypes) -> unit > when f args = > do task (async \_ -> > do args' <- mapM await args > f args') > return () > > > ... = when (\c, d -> do c.start; d.pat; asend vet c d) car dog > > That things like row polymorphism and dependant types seem *required* > to express some concepts like this in a typesafe and efficient way > suggests to me that they should be the foundation of any such safe > systems language. Especially when t in the above could be a > particular type that can't be reflected at runtime, and bitc seems to > want to have quite a few of these. > > -- > 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
