3 ms·

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 intuitivel

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]

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]