[bitc-dev] Opinions wanted: Infix shift operators

[wren ng thornton]

Jonathan S. Shapiro wrote:
> On Fri, Aug 6, 2010 at 11:33 AM, wren ng thornton <wren at freegeek.org> wrote:
> 
>> ... GHC has shown that compilers can be smart enough to
>> automatically uncurry the implementations when appropriate...
> 
> I have seen this same argument used to explain why unboxing should not be
> part of the language semantics. The problem is: this argument is only sound
> when uncurrying is elective.

I would only apply the argument to unboxing when it's elective. When 
it's non-elective, the question remains: how much of the un/boxing 
boilerplate should be forced upon the programmer? Given type signatures 
that specify the boxyness of values, having the compiler infer where to 
insert un/boxing coercions is perfectly reasonable IMO.


> When the uncurrying is mandatory (that is:
> prescriptive), it is an *error* for the compiler to *ever* emit the
> uncurried form. When this is the case, the two types
> 
>    int -> int -> int
>    int X int -> int

No, it's not an error, because it's trivial to define the higher-order 
functions necessary to coerce between them; if functions can return 
functions, then any time you define one of those functions the other is 
guaranteed to be definable. Certainly, we should not directly link the 
code of one to a call-site of the other (because that's a type error), 
but there is absolutely nothing prohibiting an indirect link via 
conversion functions.

I get the feeling we're talking past one another here. I've never 
claimed that the curried and uncurried types are identical. The only 
claim I've made (and I only made it in the previous paragraph) is that 
the types are isomorphic, and therefore there exist trivial translations 
between them.

It's perfectly fine for the FFI to use uncurried types in order to 
support direct linking against foreign code. But arity is no more a 
special part of the type here than it is for the curried form. You're 
just passing in a tuple instead of passing arguments individually; the 
number of arguments passed is the same regardless. And you always have 
all the arguments by the time the function is executed (unless you plan 
to support partial evaluation).


> Concerning, syntax, I would actually prefer the currying-style of syntax
> myself. But I think it's worth noting that there is a failure of parallelism
> in the Haskell syntax design: functions do not have arity as part of type,
> but type constructors and value constructors *do* have arity. This is
> actually fairly strange when you think about it.

That's not true. Constructor functions behave the same way as other 
functions. Partial application is just fine. You cannot pattern match on 
partially applied constructors, but you cannot pattern match on any 
other functions either.

The only situation where Haskell forbids partial application is with 
type aliases, because they are viewed in the Haskell98 report as macros 
rather than as type-level lambdas. GHC has an extension which relaxes 
this one exception.


> OTOH, the fact that it does work suggests that perhaps the problem lies in
> the arity-oblivious specification of function types rather than in the
> surface syntax of application.

It works because typed lambda calculi are in correspondence with 
Cartesian closed categories (via Curry--Howard--Lambek), and CCCs have 
natural transformations ensuring that curried and uncurried versions of 
all functions exist.



> More seriously, though, it was starting to look like there might be contexts
> in which both the type parameters and the actual parameters might be needed
> in certain function calls. If that turns out to be the case, you want the
> respective bracketing syntax to be different. It would be better, of course,
> to avoid this entirely.

All the dependently typed languages I'm familiar with use whitespace for 
type-level application without problems. You just have to generalize 
arrows to pi-types and products to sigma-types:

     A -> B    ==>    (a:A) -> B    where a takes scope over B
     A * B     ==>    (a:A) * B     where a takes scope over B

For deconstructing type terms you'd need a form of case analysis at the 
type level, since types can have multiple data constructors. E.g.,

     (x : A+B) -> case x of { Left a -> a ; Right b -> b }

And you'll have to beef up value-level case analysis in order to handle 
the local type equality constraints induced by analyzing the scrutinee. 
The best manner for doing this is still somewhat open for research. 
Coq's approach is far too weak; Agda's is the current state of the art.



>> Even if you offer curried type constructors, there's no efficiency tradeoff
>> between using curried vs uncurried, because the types are erased at
>> runtime.

Again, talking past one another. What I meant was, if we have the code

     f : C<A,B> -> D
     f = \cab -> ...

vs if we have the code

     f' : C' A B -> D
     f' = \cab -> ...

Then there is no performance difference between them, because the 
type-level application C<A,B> vs (C' A B) will be erased by runtime. 
Thus, there is no performance reason for preferring (C : Type*Type -> 
Type) over (C' : Type -> Type -> Type).

The only time there could be any performance difference in how we decide 
to name the types is if there's something prohibiting full type erasure. 
(The usual thing prohibiting full erasure is dynamic reflection, but by 
that point you've already given up on any hopes of performance, so the 
argument is moot.)


> But before I get into this any deeper, let me go read the G-machine paper
> again.

Type-level evaluation isn't really discussed there. Type-level 
evaluation only becomes interesting once you've moved to full dependent 
types or to staged computation.


>> Moreover, because types are erased, there are no constraints
>> from native calling conventions; we can call native types whatever we
>> like.
> 
> That's the problem! There *need* to be constraints imposed from the native
> calling conventions!

Whether we choose to call a type C<A,B> vs (C A B) should not have any 
impact whatsoever on native calling conventions. The name, and our 
choice of that name, is erased before we get to the point where native 
calling exists.

-- 
Live well,
~wren