Tuples are mistakenly 1-based indexed???1?!?!

[weaversa]

Frank no like.

Frank like 0-based indexing.

[brianhuffman]

In every other functional language that I've used, the components of a pair are called fst (first) and snd (second); ML also uses 1-based accessor functions #1, #2, etc. Should we buck the trend and add definitions like these to the Cryptol prelude?

zeroth : {a, b} (a, b) -> a
zeroth (x, y) = x

first : {a, b} (a, b) -> b
first (x, y) = y

[weaversa]

Frank says:

[a, b, c, d]@0 == a (a, b, c, d).1 == a Really?

Not to mention all the special cases in the source code...x !! (n-1)...and to mark '0' as an error.

[dylanmc]

I know it may sound crazy, but Cryptol version 1 also used 1-based tuple indexing:

Cryptol> :let bar = (1,2,3)
(0x1, 0x2, 0x3)
Cryptol> project(1,3,bar)
0x1

[weaversa]

Exactly! Now is the perfect time to fix all these old mistakes.

[weaversa]

Frank and I ``fixed'' this (except that now there are a bunch of new errors, sorry!) When we get a chance, we'll check in our version and submit reports for the newly induced bugs. Thanks!

[kiniry]

Aside from other complaints I have about our ad hoc tuple sub-theory, mathematical tuple projections when viewed as indices (when viewed as set-indexed products) have no a priori fixed base for the index of projection.

In fact, in various PLs you see both 0-based and 1-based projections, with perhaps 1-based projections with more regularity due to the reasons hinted at by @brianhuffman. Personally, I find 0-based indexing more elegant, as the index is then Nat and not Nat+.

We have little enough tuple-centric code that such a change would have a big impact on examples, docs, or users.

[weaversa]

There are currently no instances of tuple indexing in any of the code in the examples directory, and I only found one reference to it on page 11 of the user manual. Now seems to me like a good time to make the fix!

[brianhuffman]

The analogy between [a, b, c, d]@0 == a and (a, b, c, d).1 == a doesn't go very far.

([a, b, c, d]@i where i = 0) == a
((a, b, c, d).i where i = 1) == ??? type error

For lists/arrays, a 0-based x@i makes sense because i is an offset, a numeric value that is computed. x@i means, "start at the leftmost element of x, and move i places to the right." Tuples are completely different. In x.1 the 1 is not a value; it is a name, a label that identifies a particular slot in a data structure. For a 4-tuple, the set of indices is not Nat or Nat+; it is a set of four names: {"1", "2", "3", "4"}. Because we must always use these names directly (we can't abstract over them or compute with them) it makes sense to follow existing linguistic conventions for positionally identifying one of a small number of items.

Components of a pair are called "first" and "second", and languages like Haskell, ML and variants, F#, Scala, etc. follow this convention with fst/snd and/or 1-based tuple selectors like .1, #1 or _1.

The only mainstream language I am aware of with 0-based tuple indexing is Python, but there tuples are basically just lists, and the index is really a computed offset.

[weaversa]

The Cryptol user is prevented from doing ((a, b, c, d).i where i = 1), regardless of whether or not we've got 0 or 1-based indexing, because Cryptol's types are data independent.

A tuple is defined (in Cryptol's Haskell source) as a list. And, extracting an element is done by indexing, not names. It seems easy enough to change vs !! (n-1) to vs !! n, making the code even more elegant.

  tupleSel n v =
    case v of
      VTuple vs     -> vs !! (n - 1)

0-based indexing, I hope you agree, is the correct thing to do with respect to lists and sequences. And, it's confusing to have two different types of indexing schemes. I understand there is tradition, but I'd rather things be consistent.

[brianhuffman]

@weaversa If you're worried about elegance/consistency of Cryptol's Haskell implementation, then I think a better improvement would be to re-implement tuples as a special case of records. We should be much more concerned with consistency between tuples and records in Cryptol; arrays are totally different from either of them.

[weaversa]

I don't worry about the implementation. I worry about people being frustrated with Cryptol because of the use of multiple indexing schemes, along with many other things. We all taught a class last week and many of the issues I've been filing here are problems we found during the class. Folks complained about lists and tuples being indexed differently, and I agree. Also, as a bonus, it seems making the fix would remove some special cases from the code.

On Fri, Sep 5, 2014 at 8:24 PM, brianhuffman notifications@github.com wrote:

@weaversa https://github.com/weaversa If you're worried about elegance/consistency of Cryptol's Haskell implementation, then I think a better improvement would be to re-implement tuples as a special case of records. We should be much more concerned with consistency between tuples and records in Cryptol; arrays are totally different from either of them.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/82#issuecomment-54696436.

[dylanmc]

I agree that the "what will new Cryptol's users think" perspective is key. One datapoint that I think is pretty important is that Python uses 0-base for tuple indexing. I think helping those folks adopt Cryptol smoothly is important. And that the folks coming from Haskell or ML will be understanding. I'm glad to hear it only shows up in a couple places in the book & examples.

[brianhuffman]

I think it's about time for this thread to get an xkcd reference: http://xkcd.com/163/

[auricratio]

[Love the xkcd reference.]

Should Cryptol mistakenly continue to use 1-based indexing for tuples, I would be embarrassed to have a slide displaying both list indexing and tuple indexing. Call this a pedagogical reason for 0-based tuple indexing. :-)

[iblumenfeld]

As a cryptol user who is suffering through 1-based indices in Lua right now, I would assert that the inability to use modular operations on 1-based indices made certain, normally very simple, operations much more difficult. I argue for 0-based indices in all cases.

Ian Blumenfeld Galois, Inc. (c) 410.948.8460 ian@galois.com

On Sep 8, 2014, at 11:46 AM, Frank notifications@github.com wrote:

[Love the xkcd reference.]

Should Cryptol mistakenly continue to use 1-based indexing for tuples, I would be embarrassed to have a slide displaying both list indexing and tuple indexing. Call this a pedagogical reason for 0-based tuple indexing. :-)

— Reply to this email directly or view it on GitHub.

[kiniry]

If we stick with classic tuple projection naming semantics (which is fine with me, FWIW), then let's stop pretending that '1' is an identifier for the projection and introduce appropriate projection names and an indexing projection function in the prelude. E.g., 'first', 'second', 'third' up to some reasonable bound as Brian suggests above.

[weaversa]

The problem w/ writing projections in the prelude (or likely even special case Haskell code) is that the type system is not strong enough to allow tuples of different lengths. Cryptol does not accept, for example:

first a = a.1

It does accept,

first2(a, _) = a

But, then we'd also want to define

first3(a, _, _) = a
first4(a, _, _, _) = a

and so on. Cryptol v1 solved this problem with a 'project' function took the tuple length as the third argument. But, it was kludgy.

To throw out another potential solution Frank and I have been talking about --- how about overloading @ and ! to work on tuples, but asserting that the right-hand side be type values. (Could even thrown in @@ and !!).

[LeventErkok]

Hate to beat a dead-horse; but I think Brian nailed this one. Fields are not numbers, they are just labels. You wouldn't expect (1,2).(1+1) to mean (1,2).2, right?

Based on that, regardless you start at 0 or 1, I think calling them #1 etc. might be better, like this: (2,3,4).#3. I think this is what ML does, if memory serves. Clearly indicating in the syntax that these are not numbers.

The XKCD comic is spot on!

[kiniry]

Agreed, @LeventErkok.