I'm not too surprised. My read on SPJ is that he likes it when academic egghead ideas find practical use in the real world, and Rust has done exactly that. My mind would be blown if he said nice things about the clean design of perl or javascript, or how pre-generics java was innovative in the PL design space.
My concern with uniqueness typing was whether it is still possible to do equational reasoning. With linear function arrows this might be less of a problem. Still, if I am nasty, I can forbid the user to write x+x and force him to write 2*x instead.
I was a bit confused at 14:10 by "you can't do `write ma x; write ma y`" as that seemed to contradict the earlier important note that the linear arrow (lollipop) is not a restriction on the caller that the function can be called only once. Instead (I think) Simon is calling out an API design pattern under linear types.
There's a type error at 10:31. write should have a linear arrow on its (Int, a) argument. EDIT: Except that at 15:46 he explicitly says this isn't the case. But -XLinearTypes doesn't compile his example otherwise :thinking-face: Alternatively, we can change the type of foldl: `foldl :: (a %1 -> b -> a) -> a %1 -> [b] %1 -> a`
44:30 I'd say that it indeed is linear in x. Or actually, it may be, if the existence of y is deferred until it needs to be used. (Btw, it _kinda_ looks like strictness-laziness, doesn't it?) Also, could we get rid of that Unconstrained stuff by instead using type annotations somehow? I mean, if the point of it is to have a constructor that uses a non-linear arrow, then if we w able to specify that e.g. the linear Maybe argument has (in this case) a non-linear value inside, then to use this value multiple times, we could unwrap it from our Maybe directly, instead of additionally pattern-matching the Unconstrained bit. Now, that I think about it, maybe it would suffice to have Maybe take that constructor multiplicity as a parameter - the same way it already takes the value type as one. So for example: f :: Maybe ω Int -o Int f (Just x) = x+x -- OK g :: Maybe 1 Int -o Int g (Just x) = x+x -- Nah Btw, how to consume Nothing? Some destroy | free | black hole | …?
At 47:00 Simon mentions the better story for passing `f` to `g` is to make `f :: Int -o Int` polymorphic in arrow multiplicity. But it seems to me that such a change to `f`'s type signature ought to result in some kind of "rigid type" error. much like: `f :: Ord a=> a ; f = 'x'`
I think the reason it should work like Simon mentioned it is the following: - In `f :: Ord a=> a ; f = 'x'`: The type of `f` is actually `Char`, but the the compiler expects it to be polymorphic with the `Ord a` constraint. - In `f :: Int ₚ-> Int; f = …`: As long as "…" is indeed polymorphic to linearity, the type will in fact be true This is also much easier when you are using explicit foralls: `∀a. Ord a => a` can never be equivalent to Char, but `∀p. Int ₚ-> Int` can be equivalent to "…" (e.g. the type of `λx.5*x` or sth.).
