Robbert, Sure. I don't think it's that great — it's my first foray into paper writing — but hopefully it will have some value for you. I'm away from my computer until this evening (CST), but I'll dig it up when I next sit down at it.
I'm really glad that you've returned to Avail! We should catch up again soon. I'm currently working on the web-side of Avail (i.e., a good JavaScript client for the Avail server), which is important if not glamorous. Todd > On Jan 6, 2015, at 8:50 AM, Robbert van Dalen <[email protected]> > wrote: > > dear Todd, > > can i have a copy of your paper please? > > thank you, > > - robbert > >> On 06 Jan 2015, at 15:48, Todd L Smith <[email protected]> wrote: >> >> Mark, >> >> You seem to have meant [⊥'s type, ⊥'s type]→boolean in the last paragraph. I >> only had time to skim after shoveling snow, but I think I understood well >> enough to catch your intent. >> >> Todd >> >>> On Jan 6, 2015, at 1:32 AM, Mark van Gulik <[email protected]> wrote: >>> >>> Robbert, >>> >>> Ok, I finally skimmed it. One thing I would recommend for performance is >>> in the implementation of “_is comparable with_” for tuple types (lines >>> 86-105). Before doing the expensive (at compile-time) loop over >>> corresponding elements, you may want to optimize for the common case of >>> mostly-homogenous tuples. Primitive 143 is made available as the method >>> "∪_[_.._]”. This takes a tuple type, a natural number [1..∞), and a >>> non-negative extended integer [0..∞]. All element types of the tuple type >>> in the specified subscript range are efficiently type-unioned to form the >>> result. Any subscripts that would be out of bounds are efficiently >>> ignored. So you could add a line to the start of the block (line 92) like: >>> >>> if ∪t1[1..∞] is comparable with ∪t2[1..∞] then [Exit body with true]; >>> >>> That hinges on the assumption that having more precise type information >>> should not make things incomparable that would otherwise be comparable. If >>> that’s the case, you can also make the leaf cases (number and character) of >>> “_is comparable with_” effectively final by removing the “ : boolean” after >>> the close square brackets on lines 79 and 84. Technically, the method can >>> truly be sealed with “Seal method_at_” at those coordinates in the >>> signature lattice, to prevent other modules from strengthening them further >>> (say, by a mischievous or malicious coder making the strings “apples” and >>> “oranges” be incompatible – but no other strings). >>> >>> Oh, and now that I’m looking more closely at it, line 94 through 100 are >>> probably wrong for the case that one tuple type reaches its homogenous >>> point at an earlier subscript than the other tuple type. It’s probably >>> easier to just subscript the tuple types themselves without building the >>> leading + <default> tuples. Note that the leading + <default> tuples can >>> disagree in length even when the tuple types are constrained to be the same >>> fixed size. Consider <1,1>’s type and <1,2>’s type, for example. The >>> leading + <default> of the first is <1’s type>, but for the second it’s >>> <1’s type, 2’s type>. We’ve been bitten by that anti-intuitive situation >>> multiple times in the past. >>> >>> Finally, you might want to add an implementation of “_is comparable with_” >>> for [⊥,⊥]→boolean. It’s up to you whether it should answer true or false, >>> since it’s impossible to actually invoke a comparison on an instance of ⊥ – >>> because there aren’t any! But such a method definition might help to >>> simplify the code that deals with running off the end of one of the tuple >>> types. And even though “_is comparable with_” is currently private, it’s >>> possible that it might be exposed by a subsequent refactor. In that world, >>> invoking it with <⊥,⊥> is perfectly reasonable – and would lead to an >>> ambiguous lookup exception at runtime without the proposed definition. >>> >>> Everything else that I skimmed seemed fine. >>> >>> -Mark >>> >>> >>>> On Jan 4, 2015, at 12:55 PM, Robbert van Dalen >>>> <[email protected]> wrote: >>>> >>>> hi, >>>> >>>> i’ve just finished a generic tuple ordering implementation - as promised. >>>> see: https://github.com/rapido/spread/blob/master/avail/ordering.avail >>>> >>>> please feel free to suggest alternatives. >>>> >>>> and yes please, i would like to have a copy of todd’s paper! >>>> >>>> cheers, >>>> Robbert. >>>> >>>>> On 04 Jan 2015, at 06:18, Mark van Gulik <[email protected]> wrote: >>>>> >>>>> Todd wrote a very interesting paper about statically checking in a way >>>>> that’s sort of orthogonal to the type system. It didn’t get accepted for >>>>> publication, however, mostly because of its dependence on novel features >>>>> of Avail. He or I can send you a copy if you want, although it might >>>>> contain some spoilers :-). >>>>> >>>>> >>>>>> On Jan 3, 2015, at 12:25 PM, Robbert van Dalen >>>>>> <[email protected]> wrote: >>>>>> >>>>>> thank you for taking your time discussing this. >>>>>> >>>>>>> Having read the indicated section at the link you provided (and the >>>>>>> rest of the page), it appears that Avail’s object types are a close fit >>>>>>> for implementing extensible records >>>>>> >>>>>> indeed, after reading your elaborate exposition of the avail object type >>>>>> system, it appears that they are a close fit. >>>>>> however, there is one snag: object fields have no natural ordering, >>>>>> whilst tuple fields obviously do (i could be wrong). >>>>>> >>>>>> while the notion of equality in avail is very well designed and first >>>>>> class, i believe that ordering (less than, greater than) is less >>>>>> developed. >>>>>> for instance, i would like to be able to order tuples (if they contain >>>>>> elements that can also be ordered). next to that, there are no primitive >>>>>> ordered sets or maps. >>>>>> >>>>>> one challenge i’d like to take on is whether it is possible to implement >>>>>> a generic avail library that can order almost everything out-of-the-box, >>>>>> without any boilerplate. >>>>>> note that in scala, (boilerplate free) generic ordering can be achieved >>>>>> via implicits; in haskell, via type classes. >>>>>> >>>>>> probably, you or todd can implement such library in a day or so. >>>>>> but please don’t. let me have a stab at it - in order for me to learn >>>>>> more about avail. >>>>>> >>>>>> cheers, >>>>>> >>>>>> - robbert >>> >
