1-tuples

[davidweichiang]

Is it bad that we have no way of writing the type of 1-tuples of either kind? Especially since <e> really is different from e because it’s linear?

[colin-mcd]

I will admit that I'm a little reluctant to allowing 1-tuples of either kind; I don't think they actually enforce linearity, and if you really wanted to enforce the linear use of something, you could always put it in a thunk (Unit -> A).

*-tuples are robust so long as all their components are, so a *-tuple of one thing is basically the same as that thing anyway.

Currently, &-tuples are never robust in that you may only ever use them once. However, in a sense you can use one multiple times so long as you only ever use the same (robust) component. You can do this by putting that component in a let-definition, e.g. let d = e.3 in ... and then use d (and hence, e.3) multiple times in ....

Does this make sense?

[davidweichiang]

Does this mean that (for example) in the refunctionalization transform, you have to have a special case that changes into A?

Hmm... I suspect there probably is a corner case where if you only have a constructor with free variables once or do a case-of with a free variable inside it once, the de-/refunctionalized code will have some 1-tuples. For the sake of outputting an FGG it probably works fine (all the code except the parser and pretty-printer should still work fine for 1-tuples), but if you only compile to an intermediate stage, the outputted code may not parse.

[ccshan]

I don't see anything wrong with allowing the Python-like syntax of (e,) for parsing and pretty-printing...

[davidweichiang]

I think it'd also be okay to implement <e> but but not (e,).

It does seem a little weird that the command-line interface exposes the intermediate form but the intermediate form might not be parseable, so I'd vote for doing whatever fixes that.

[davidweichiang]

Related, should we allow ()?

[davidweichiang]

(I think we should allow ()).

[davidweichiang]

It looks to me like

• <e> is allowed, so any intermediate code output by refunctionalization still compiles
• none of the internal program transformations produce multiplicative 1-tuples ((e,)), so we don't really need syntax for that

I just made PR #55 which allows (). However, in the generated FGG, the type of empty tuples is "" because we have no way of writing the type of empty tuples. Should we just follow the paper and make a built-in type called Unit with the single inhabitant ()?

[davidweichiang]

I'd also be fine with the Haskell way -- (Bool, Bool) instead of Bool * Bool and <Bool, Bool> instead of Bool & Bool.

[davidweichiang]

Related, the following code

let (x) = False in True

produces the cryptic error message

Failed to unify Bool and ?0, in the expression let (x) = False in True

I think (x) might be a 1-tuple here?

[colin-mcd]

Related, the following code

let (x) = False in True

produces the cryptic error message

Failed to unify Bool and ?0, in the expression let (x) = False in True

I think (x) might be a 1-tuple here?

That sounds right... (x) is a 1-tuple and type inference tries to unify the type of False--Bool--with the as-of-yet unsolved 1-tuple (?0) (?n are type inference-introduced variables, which all get solved to real types in a well-typed program). But Bool isn't a tuple at all, so it fails to unify. I'm not sure why it is saying that it tried to unify Bool and ?0 instead of (?0)--is it possible that the pretty-printer prints 1-tuples without parentheses?

[davidweichiang]

I'm still okay with the decision to allow unary &-tuples but not unary *-tuples. However, we still have no way of writing the type of <e>, so this will prevent compilation of generated code that uses <e>.

[ccshan]

I'm still okay with the decision to allow unary &-tuples but not unary *-tuples.

Me too.

However, we still have no way of writing the type of <e>, so this will prevent compilation of generated code that uses <e>.

Is there any syntactic (parsing or printing) reason to not go the Haskell way of writing <t1,t2> instead of t1&t2 (and writing (t1,t2) instead of t1*t2)? In papers and in Haskell, the reason is not syntactic but more conceptual: when computation on types is allowed, we might want to compute with a pair of types, which would have the kind Type*Type, and is distinct from a type of pairs, which would have the kind Type.

[davidweichiang]

Yeah, I think we should give that a try. Would have saved us a lot of discussion.

[davidweichiang]

Regarding changing the types to use (...) and <...>, are there any negative consequences for () to be both a type and a term, and likewise for <>?

[ccshan]

Regarding changing the types to use (...) and <...>, are there any negative consequences for () to be both a type and a term, and likewise for <>?

I don't expect any. I understand the current proposal to be allowing unary additive tuples such as <()>, whose type is <()>, but NOT unary multiplicative tuples. In particular, (()) means the same as () both as term and as type.

[davidweichiang]

Right. I'm trying it out now.