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.
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`
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.
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.).
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 | …?
Wherever you want to use subtyping -- NAUGHTY; use polymorphism instead. -- SPJ
Or destroy the world, which is known to be undesirable. -- SPJ
32:57
"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.
i just noticed that all his talks are made with comic sans love it lol
We can still use function application and pattern match syntax with linear types. So, this syntax is somehow overloaded.
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`
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.
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
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.).
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 | …?
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
Next step is to rewrite Haskell's runtime library into Rust, or what? :-)