alt Hacker NewsSo why does the length function take the ‘a’ parameter (the type of the elements?) and its Kind? Wouldn’t the type imply the kind? Why does the kind matter? Is the - a constraint on the kind? How would the program be different without the -?
When you say “pair type former” do you mean that Array<U32> & U32 is what Rust would call (Array<U32>, U32)? If so, why does that example function actually return a value of this type? It sure looks like it returns plain U32.
> You can use an erased argument as many times as you want, in erased positions.
What’s the rationale for this? Why is an “erased” position special? What is an erased position, anyway?
ISTM if I want to use an affine term that has zero size at runtime as a token that may be used at most once, I think I wouldn’t want an exception for using it in an “erased” position. Can I have a function like a -> a & a where the input is “erased”?
Ohhh. Ok. I see the confusion. That's bad syntax then. The 'a' parameter is not the type of the elements. 'A' is the type of the elements. 'a' is just the "quantity of the type of the type of the elements". Yes, that's a mouthful, and somewhat abstract. This is similar to Agda's universe polymorphism. The reason it exists is because there are two "types of types" (i.e., kinds). Copiable types, and non-copiable types. So, this argument allows you to parametrize a function on both of these kinds. That way, you don't need to write List.length twice: one for copiable types, and once for non-copiable types. Think of Rust generics. 'a' is playing the same role as a "Copiable" trait would in Rust. It is just an extra compile-time argument to avoid boilerplate. But yes, I see how this can be confusing and I think I know how to improve that syntax.
Yes, `Array<U32> & U32` is just `(Array<U32>, U32)` and now that you point it I believe I made a bad choice, no excuses. Also, `arr[3]` doesn't return a number. It returns a copy of the same array, plus a number. So, if the element at index 3 is 123, tthen, `arr[3]` will return `(arr, 123)`. Now, you might be thinking: that's terrible. And yes, it is. I realize it now. I should have made the `arr[3]` syntax return 123. It is there for a very good reason though. It preserves linearity. It is part of the termination argument that makes Bend consistent. But yes, exposing it to the end user was most likely a mistake. I will redesign that syntax. Sorry about it.