4 ms·

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 typ

by 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]

by platz 4y ago

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]