Home » forums » LtU Forum

if Records - Labels = Tuples then Rows - Labels = what?

I have been reading up on row/record polymorphism (thanks to Andreas and Daniel for the pointers), but so far I haven't seen anything which apply the concept of a row variable to tuples.

If I understand my theory correctly, record types without labels are in fact tuples (or product types if you prefer). So if you have a row without labels, what would that be? An "unlabeled row"?

Viewed from another angle, I want to describe tuples with row variables. The nitty gritty of the whole thing is that I am working on devising an acceptable way to describe stack configurations using type theory.

A stack with an integer on top, and anything else on the bottom can be described as: 

  T = int * A

where A is the "unlabelled row variable". Perhaps these are examples of "stack types" or I could call them "column types" to distinguish them from rows?

Any ideas or suggestions would be much appreciated!

By cdiggins at 2006-11-18 19:54 | LtU Forum | previous forum topic | next forum topic | other blogs | 6506 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

SML

In SML tuples are records labeled by natural (or positive?) numbers. So
int * int = {1:int,2:int}.

[on edit, also corrected kind/sort typo. note to self never write about type systems after more than 36 hours without sleeping]
A row has the semantics you define it to have. It's important to understand that a row isn't a type, it's in the same level of kind * (i.e. both have sort ◻. Actually it can be defined in other levels, even in something like row : foo : bar : ◻, but I digress). So if we have an unlabeled row (|int,int|) and two operations Var, Rec :: row -> type we can use this row to define unlabeled records (i.e. tuples) and unlabeled unions (which is something that doesn't exist in most languages). IMO it's better to provide labeled rows, products and sums, defining the unlabeled versions as syntatic sugar for numeric labels, because the labels provide additional information that is useful to the developer. Categorically speaking this is true <left:int,right:unit> = <just:int,nothing:unit> (where = is up to isomorphism) but the former hides the intent. With unlabeled sums you have only <int,unit> which doesn't give any information. Worse it could be <int,int> which can be a great source of confusion.

By Daniel Yokomizo at Sat, 2006-11-18 20:39 | login or register to post comments

Gaster and Jones

I see what you are saying about a row not being a type. I didn't realize there was a distinction. I am a bit confused though by your statement about types and rows having the same kind. In the Gaster and Jones paper http://citeseer.ist.psu.edu/gaster96polymorphic.html, referenced by the Leijen paper you pointed me to, it indicates that types and rows are distinguished by having different kinds. Types are defined by their grammar as having kind "*" while rows have kind "row". Can you help clarify?

These are very important concepts you are pointing me to, and I really appreciate your help!

By cdiggins at Sat, 2006-11-18 22:07 | login or register to post comments

Kind of rows

I suppose Daniel just made some kind of typo. It is as you say: rows have a kind different from proper types.

Regarding rows for tuples: if you are not interested in labels then just define rows as (ordered) lists of types for your application. That is:

kind ::= Type | Row
type ::= a | int | (row)->(row) | forall a:kind.type | ...
row ::= a | nil | type,row

(You can also put types and rows in the same syntactic category and let only the kind system differentiate, but that's a matter of taste.)

By Andreas Rossberg at Sun, 2006-11-19 09:04 | login or register to post comments

And Now for Something Completely Different

As Andreas noted...

I suppose Daniel just made some kind of typo.

Kind of. I was thinking in terms of PTS. In a PTS you have int : * : ◻ and (|x:int|) : row : ◻ so they have different kinds but these kinds have the same sort (i.e. ◻). I can't think of rows disassociated from PTS since I spent a couple of months trying to come with a PTS with higher-kinded rows (i.e. one where you can write (|x:int,y:*,z:row|)).

By Daniel Yokomizo at Sun, 2006-11-19 15:07 | login or register to post comments

Just out of interest, how

Just out of interest, how were you encoding rows and records, assuming you weren't simply extending the PTS framework?

By Philippa Cowderoy at Mon, 2006-11-20 15:48 | login or register to post comments

I was simply extending it

I was simply extending it because I wanted a nice correspondence with basic logic algebra (i.e. & = Rec, | = Var, true = unit, false = bottom*, -> = Pi).

[on edit]
*by bottom I meant non-returning values (e.g. continuations), instead of all divergent computations.

By Daniel Yokomizo at Mon, 2006-12-04 01:57 | login or register to post comments

IMO it's better to provide

IMO it's better to provide labeled rows, products and sums, defining the unlabeled versions as syntatic sugar for numeric labels, because the labels provide additional information that is useful to the developer.

In general I agree with this sentiment, however in the case of the Cat language, the semantics are purposefully minimalist. Cat is a very simple functional stack-based language, and I am trying to formalize the semantics and retain a Forth-like simplicity to the whole thing.

By cdiggins at Mon, 2006-11-20 06:27 | login or register to post comments

That is not dead, which can eternal lie...

The question is ill-defined, but I suppose the morally correct answer is that a row without labels is simply a finite multiset of types, or, if you allow row variables, a 'monotonic' function between such.

If what the poster seeks is a pat term for such a beast, I do not know of one. (But just because it has no name doesn't mean it doesn't exist.)

By Frank Atanassow at Mon, 2006-11-20 16:48 | login or register to post comments