5 ms·

why is it weird; a breif description of the observation would be helpful

by platz 4y ago

chpatrick 4y ago
Because at first glance it looks like it produces a value of type Either (b -> c) b out of "thin air". (Really it comes from the continuation but intuitively it looks unusual).
- hgsgm 4y ago
  Are you saying it's weird that a function has an explicit type in Haskell? ("First-class" functions) https://en.m.wikipedia.org/wiki/First-class_function https://en.m.wikipedia.org/wiki/First-class_function
  - mrkeen 4y ago
    You can read those lower case letters as preceded by "for all", and it's up to the caller to choose which concrete type the letter should represent, as the function promises to return an implementation "for all" concrete types. So if wrote the function foo, foo :: Int -> b and you happened to need a BufferedReader, you could just get it by calling (foo 3). That's what the "thin air" comment is. Where could the implementation of BufferedReader possibly have come from?
    - gowld 4y ago
      That's impossible, but that's not what's happening here. There is no "-> b" at the end of the type signature upthread. The example in the thread is more like foo :: Either (b -> Int) b which is much easier: foo = Left (const 1) :: Either (b -> Int) b
- platz 4y ago
  Cont r a is a CPS computation that produces an intermediate result of type "a", within a CPS computation whose final result type is "r" In your example of type "Cont c (Either (b -> c) b)", it produces a final value of type "c". (There is no Either in the final result, i.e. there is no "excluded middle") It produces an intermediate result of type (Either (b -> c) b) by feeding values through Left and Right constructors, calling the continuation multiple times, once for Left and once for Right. I don't see what you mean by "thin air" because the Left and Right constructors in the definition are creating the Either, first creating the Right, and then feeding that result to the Left. If you think the (Either (b -> c) b) is the final result, then you don't understand or are misrepresenting the meaning of the definition of Cont r a (don't make the mistake of thinking the final result is of type "a". it is of type "r") There is no excluded middle here. It just uses the Either as a way to encode & pass 2 different functions to the continuation. The naming of the function as "excludedMiddle" is disingenuous.
  - chpatrick 4y ago
    Actually I called it that because it's derived from the law of excluded middle: "A OR not A" is always true. You can encode logical statements in the Haskell type system as follows: a OR b: Either a b a AND b: ( a, b ) not A: a -> Void a implies b: a -> b With this encoding, having a well-formed value for a given type is a proof of its validity. The one thing we can't use directly is double negation, because we would have to make A appear out of nowhere: ((a -> Void) -> Void) -> a However, this is exactly the type of Cont Void. This means we can use the Cont Void monad to make logical proofs, including double negation. The type: Cont Void (Either (a -> Void) a)) Encodes the law of excluded middle, and the value I wrote is a proof of it. It so happens that you can use a type parameter instead of Void because an arbitrary type can also not be used for anything.
    - gowld 4y ago
      > ((a -> Void) -> Void) -> a > However, this is exactly the type of Cont Void. Defined where? Not here: https://hackage.haskell.org/package/monads-tf-0.1.0.3/docs/Control-Monad-Cont.html https://hackage.haskell.org/package/monads-tf-0.1.0.3/docs/C... https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Cont.html https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-M... The closest I find is cont :: ((a -> r) -> r) -> Cont r a so cont (a -> Void) -> Void) :: Cont Void a There is nothing "out of thin air", since `a` is the input, not the ouput, unless you just misread the type. But that can be said for any higher-order type, like map :: (a -> b) -> [a] -> [b]
tel 4y ago
A value of type forall a b. Either (a -> b) a is particularly dangerous because we can pick b to be uninhabited (Void) forall a. Either (a -> Void) a which is the law of excluded middle, for any type we either can immediately summon an example or prove that no example exists, as having a function (A -> Void) would allow us to create a value of the uninhabited type if we had a value of A. But forall r a. Cont r (Either (a -> r) a) is fine. Let's see what happens when we set c = Void and unwrap the Cont lem : forall r a. Cont r (Either (a -> r) a) runCont lem @Void : forall a. (Either (a -> Void) a -> Void) -> Void It turns into a weird statement, a double-negation, that there exists no proof that (Either (a -> Void) a), the true LEM type, is uninhabited. Not the same as actually having such a value. Consider the challenge of constructing (Either (A -> Void) A -> Void) for different types A. Let's say you have a positive capability of generating values of type A. This is constructive proof that (A -> Void) cannot exist so you know that any caller of your function will give you (Right value) if they are capable of calling you at all. That's not particularly helpful since you're on the hook to generate an uninhabited type Void, now. Alternatively, let's say you lack a method to construct values of A. Now either you (a) never get called, (b) get called with a parameter like (Right value), proving to you that values of A exist but asking you to use one to produce a value of type Void (impossible!), or (c) you get a value of type (Left fn), which constructively proves that no values of type A can be constructed. So in this double-negative formulation, allowing for the potential that you simply never get called, nothing about this LEM-like type is problematic. But it sure looks close to something dangerous. --- You can see how this construction works by stripping away the Cont wrapper. runCont (cont f) = f runCont (cont (\c -> (c . Left) (c . Right))) = \c -> (c . Left) (c . Right) \c -> (c . Left) (c . Right) lem :: forall a . (Either (a -> Void) Void -> Void) -> Void lem c = c (Left (\x -> c (Right x))) So we see that our callback, discussed above, is always called with a value of shape (Left fn), which appears to be a constructive proof that no values of type `a` exist. It works via a trick, though. If you were to attempt to disprove the statement of that function (a -> Void) by offering it a value of type `a`, that function will just use the value you constructed and hand it back to you as (Right value), forcing you to yourself prove (a -> Void). This is messy circular logic, but common in this kind of construction. The only way to "construct a value" of Void is to somehow pass the buck and force someone else to do it. And so this formulation of "LEM" does just what it says on the tin: shows that it's impossible to prove that LEM is impossible. Any such proof can be turned against itself.

why is it weird; a breif description of the observation would be helpful

by platz 4y ago

why is it weird; a breif description of the observation would be helpful

Because at first glance it looks like it produces a value of type Either (b -> c) b out of "thin air". (Really it comes from the continuation but intuitively it looks unusual).

hgsgm 4y ago
Are you saying it's weird that a function has an explicit type in Haskell? ("First-class" functions) https://en.m.wikipedia.org/wiki/First-class_function https://en.m.wikipedia.org/wiki/First-class_function
- mrkeen 4y ago
  You can read those lower case letters as preceded by "for all", and it's up to the caller to choose which concrete type the letter should represent, as the function promises to return an implementation "for all" concrete types. So if wrote the function foo, foo :: Int -> b and you happened to need a BufferedReader, you could just get it by calling (foo 3). That's what the "thin air" comment is. Where could the implementation of BufferedReader possibly have come from?
  - gowld 4y ago
    That's impossible, but that's not what's happening here. There is no "-> b" at the end of the type signature upthread. The example in the thread is more like foo :: Either (b -> Int) b which is much easier: foo = Left (const 1) :: Either (b -> Int) b
platz 4y ago
Cont r a is a CPS computation that produces an intermediate result of type "a", within a CPS computation whose final result type is "r" In your example of type "Cont c (Either (b -> c) b)", it produces a final value of type "c". (There is no Either in the final result, i.e. there is no "excluded middle") It produces an intermediate result of type (Either (b -> c) b) by feeding values through Left and Right constructors, calling the continuation multiple times, once for Left and once for Right. I don't see what you mean by "thin air" because the Left and Right constructors in the definition are creating the Either, first creating the Right, and then feeding that result to the Left. If you think the (Either (b -> c) b) is the final result, then you don't understand or are misrepresenting the meaning of the definition of Cont r a (don't make the mistake of thinking the final result is of type "a". it is of type "r") There is no excluded middle here. It just uses the Either as a way to encode & pass 2 different functions to the continuation. The naming of the function as "excludedMiddle" is disingenuous.
- chpatrick 4y ago
  Actually I called it that because it's derived from the law of excluded middle: "A OR not A" is always true. You can encode logical statements in the Haskell type system as follows: a OR b: Either a b a AND b: ( a, b ) not A: a -> Void a implies b: a -> b With this encoding, having a well-formed value for a given type is a proof of its validity. The one thing we can't use directly is double negation, because we would have to make A appear out of nowhere: ((a -> Void) -> Void) -> a However, this is exactly the type of Cont Void. This means we can use the Cont Void monad to make logical proofs, including double negation. The type: Cont Void (Either (a -> Void) a)) Encodes the law of excluded middle, and the value I wrote is a proof of it. It so happens that you can use a type parameter instead of Void because an arbitrary type can also not be used for anything.
  - gowld 4y ago
    > ((a -> Void) -> Void) -> a > However, this is exactly the type of Cont Void. Defined where? Not here: https://hackage.haskell.org/package/monads-tf-0.1.0.3/docs/Control-Monad-Cont.html https://hackage.haskell.org/package/monads-tf-0.1.0.3/docs/C... https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Cont.html https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-M... The closest I find is cont :: ((a -> r) -> r) -> Cont r a so cont (a -> Void) -> Void) :: Cont Void a There is nothing "out of thin air", since `a` is the input, not the ouput, unless you just misread the type. But that can be said for any higher-order type, like map :: (a -> b) -> [a] -> [b]

tel 4y ago

A value of type forall a b. Either (a -> b) a is particularly dangerous because we can pick b to be uninhabited (Void) forall a. Either (a -> Void) a which is the law of excluded middle, for any type we either can immediately summon an example or prove that no example exists, as having a function (A -> Void) would allow us to create a value of the uninhabited type if we had a value of A. But forall r a. Cont r (Either (a -> r) a) is fine. Let's see what happens when we set c = Void and unwrap the Cont lem : forall r a. Cont r (Either (a -> r) a) runCont lem @Void : forall a. (Either (a -> Void) a -> Void) -> Void It turns into a weird statement, a double-negation, that there exists no proof that (Either (a -> Void) a), the true LEM type, is uninhabited. Not the same as actually having such a value. Consider the challenge of constructing (Either (A -> Void) A -> Void) for different types A. Let's say you have a positive capability of generating values of type A. This is constructive proof that (A -> Void) cannot exist so you know that any caller of your function will give you (Right value) if they are capable of calling you at all. That's not particularly helpful since you're on the hook to generate an uninhabited type Void, now. Alternatively, let's say you lack a method to construct values of A. Now either you (a) never get called, (b) get called with a parameter like (Right value), proving to you that values of A exist but asking you to use one to produce a value of type Void (impossible!), or (c) you get a value of type (Left fn), which constructively proves that no values of type A can be constructed. So in this double-negative formulation, allowing for the potential that you simply never get called, nothing about this LEM-like type is problematic. But it sure looks close to something dangerous. --- You can see how this construction works by stripping away the Cont wrapper. runCont (cont f) = f runCont (cont (\c -> (c . Left) (c . Right))) = \c -> (c . Left) (c . Right) \c -> (c . Left) (c . Right) lem :: forall a . (Either (a -> Void) Void -> Void) -> Void lem c = c (Left (\x -> c (Right x))) So we see that our callback, discussed above, is always called with a value of shape (Left fn), which appears to be a constructive proof that no values of type `a` exist. It works via a trick, though. If you were to attempt to disprove the statement of that function (a -> Void) by offering it a value of type `a`, that function will just use the value you constructed and hand it back to you as (Right value), forcing you to yourself prove (a -> Void). This is messy circular logic, but common in this kind of construction. The only way to "construct a value" of Void is to somehow pass the buck and force someone else to do it. And so this formulation of "LEM" does just what it says on the tin: shows that it's impossible to prove that LEM is impossible. Any such proof can be turned against itself.