Alice ✨
@welltypedwit.ch
When the limestone of imperative programming has worn away, the granite of functional programming will be revealed underneath -Simon Peyton Jones
https://welltypedwit.ch
https://welltypedwit.ch
sorry, i don't believe in capitalist ideas like ownership
November 11, 2025 at 10:12 AM
sorry, i don't believe in capitalist ideas like ownership
why would it need a gc? you would just need a statically initialized default value for every type (and if you have a guarantee that default values always have bit pattern 0, you only need a single 0 array as large as your largest type)
November 11, 2025 at 10:08 AM
why would it need a gc? you would just need a statically initialized default value for every type (and if you have a guarantee that default values always have bit pattern 0, you only need a single 0 array as large as your largest type)
yeah but references are silly so
November 11, 2025 at 10:05 AM
yeah but references are silly so
worse: that's a type error because the expression `f : (a b : Nat) -> Nat` still has type `(x y : Nat) -> Nat` and so doesn't have a parameter named "a"
November 11, 2025 at 2:20 AM
worse: that's a type error because the expression `f : (a b : Nat) -> Nat` still has type `(x y : Nat) -> Nat` and so doesn't have a parameter named "a"
oh I guess that is what would happen if you used records as arguments huh
November 11, 2025 at 1:55 AM
oh I guess that is what would happen if you used records as arguments huh
why would you expect the second and third one to return 1?
November 11, 2025 at 1:53 AM
why would you expect the second and third one to return 1?
oh I didn't even consider that that would happen if you passed everything positionally!
you're right about the first part, but in the second one it's actually that (f : (y x : Nat) -> Nat) is inferred to `(x y : Nat) -> Nat` because that is the type of `f`
you're right about the first part, but in the second one it's actually that (f : (y x : Nat) -> Nat) is inferred to `(x y : Nat) -> Nat` because that is the type of `f`
November 11, 2025 at 1:52 AM
oh I didn't even consider that that would happen if you passed everything positionally!
you're right about the first part, but in the second one it's actually that (f : (y x : Nat) -> Nat) is inferred to `(x y : Nat) -> Nat` because that is the type of `f`
you're right about the first part, but in the second one it's actually that (f : (y x : Nat) -> Nat) is inferred to `(x y : Nat) -> Nat` because that is the type of `f`
(it's 1 but that depends on the detail that the type checker "prefers" the then branch in an if)
November 11, 2025 at 1:19 AM
(it's 1 but that depends on the detail that the type checker "prefers" the then branch in an if)
also, 122 would be reasonable in this case, but would still be problematic in general. e.g. what does this print?
def f(x y : Nat): Nat := x
def g(y x : Nat): Nat := y
def h := if false then f else g
#eval h (x := 1) (y := 2)
def f(x y : Nat): Nat := x
def g(y x : Nat): Nat := y
def h := if false then f else g
#eval h (x := 1) (y := 2)
November 11, 2025 at 1:19 AM
also, 122 would be reasonable in this case, but would still be problematic in general. e.g. what does this print?
def f(x y : Nat): Nat := x
def g(y x : Nat): Nat := y
def h := if false then f else g
#eval h (x := 1) (y := 2)
def f(x y : Nat): Nat := x
def g(y x : Nat): Nat := y
def h := if false then f else g
#eval h (x := 1) (y := 2)
wait really? even though g's type uses `y x`, you would want to expose that its implementation happens to be defined in terms of a function that uses `x y`?
November 11, 2025 at 1:15 AM
wait really? even though g's type uses `y x`, you would want to expose that its implementation happens to be defined in terms of a function that uses `x y`?
because lean wants to have its cake (have named arguments) and eat it too (make alpha equivalent function types equal) but that exposes weird implementation details like the order of unification and how here the type ascription apparently isn't used for the named argument applications
November 11, 2025 at 1:07 AM
because lean wants to have its cake (have named arguments) and eat it too (make alpha equivalent function types equal) but that exposes weird implementation details like the order of unification and how here the type ascription apparently isn't used for the named argument applications
it doesn't override the named argument in the third case though!
November 11, 2025 at 1:01 AM
it doesn't override the named argument in the third case though!
what if i told you that it's 121 ^^
November 11, 2025 at 12:14 AM
what if i told you that it's 121 ^^
(this is why vega doesn't have named arguments btw)
November 11, 2025 at 12:01 AM
(this is why vega doesn't have named arguments btw)
and if so, does that mean that `StateT Parallelizable ...` won't actually run anything in parallel? (because the applicative instance for StateT needs to use the monad instance of the underlying monad)
November 10, 2025 at 5:38 PM
and if so, does that mean that `StateT Parallelizable ...` won't actually run anything in parallel? (because the applicative instance for StateT needs to use the monad instance of the underlying monad)
oh that's really cool! am i understanding this correctly that you're essentially doing the validation thing where your monad instance isn't lawful because Applicative would run things in parallel, but Monad would run them serially?
November 10, 2025 at 5:38 PM
oh that's really cool! am i understanding this correctly that you're essentially doing the validation thing where your monad instance isn't lawful because Applicative would run things in parallel, but Monad would run them serially?
it means a non-dependent function is a function that isn't dependent
November 9, 2025 at 2:47 PM
it means a non-dependent function is a function that isn't dependent
(and also i'm not sure computer scientists necessarily realize that they're usually using a different definiton of tree than graph theorists)
November 9, 2025 at 12:50 PM
(and also i'm not sure computer scientists necessarily realize that they're usually using a different definiton of tree than graph theorists)
yes, although i was more getting at the difference between trees and *rooted* trees (usually rooted trees are still phrased as undirected but with a distinct root, aren't they?)
i just used this in a graph theory proof and the computer scientist in me felt really weird about it ^^
i just used this in a graph theory proof and the computer scientist in me felt really weird about it ^^
November 9, 2025 at 12:50 PM
yes, although i was more getting at the difference between trees and *rooted* trees (usually rooted trees are still phrased as undirected but with a distinct root, aren't they?)
i just used this in a graph theory proof and the computer scientist in me felt really weird about it ^^
i just used this in a graph theory proof and the computer scientist in me felt really weird about it ^^
what is your definition of a leaf? ^^
November 9, 2025 at 12:42 PM
what is your definition of a leaf? ^^