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.).
Wherever you want to use subtyping -- NAUGHTY; use polymorphism instead. -- SPJ
i just noticed that all his talks are made with comic sans love it lol
Or destroy the world, which is known to be undesirable. -- SPJ
"Polymorphism!". I didn't see it coming and the suspense was killing me.
SPJ lauding Rust for it’s type system. Wow.
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.
We can still use function application and pattern match syntax with linear types. So, this syntax is somehow overloaded.
44:28 - so it is not working in GHC 9.0.1 what extension should I use?
What a surprise when I discovered that reproduction velocity was normal and not 1.25
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.
newMArray makes the created ma linear. The statements aren't just standalone but rather somewhere in the function passed to newMArray.
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`
The `read2` example furthermore needs a CPS transformation (with type signatures) to compile:
```
read2 :: MArray Int %1 -> Int -> (MArray Int, Unrestricted Int)
read2 ma n = f' (read ma n)
where
f' :: (MArray Int, Unrestricted Int) %1 -> (MArray Int, Unrestricted Int)
f' !(ma1, Unrestricted v2) = g' (read ma1 (n + 1)) v2
g' :: (MArray Int, Unrestricted Int) %1 -> Int -> (MArray Int, Unrestricted Int)
g' !(ma2, Unrestricted v2) v1 = (ma2, Unrestricted (v1 + v2))
```
I can't for the life of me figure out how `foldl` has type `(a %p -> b %q -> a) -> a %p -> [b] %q -> a`
Now we're cooking with gas. -- SPJ
I had a postdoctoral advisor who used to say this expression all the time. Must be the same generation.
english stackexchange q 25897
Interesting! Thanks
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.).
Next step is to rewrite Haskell's runtime library into Rust, or what? :-)