7 ms·

The Soft Side of Software

102 points by k4rtik 9y ago

zengid 9y ago
Can anyone help me interpret the type signature Meijer used in his programming question? "Given a generic type: Cont r a = (a -> r) -> r Prove that this type forms a monad." I'm reading it as 'Container' passed 'r' and 'a' performs 'a' to 'r' which returns 'r'. (I'm guessing on verbs here).. I've never come across a good way to read these type signatures.
- bjl 9y ago
  I read this as 'A cont of type r a is a function that, given a function of type a to r, returns an r'.
- hdhzy 9y ago
  Cont refers to the continuation monad. For details see http://www.haskellforall.com/2012/12/the-continuation-monad.html http://www.haskellforall.com/2012/12/the-continuation-monad....
- wz1000 9y ago
  Cont stands for Continuation. A continuation basically represents a 'suspended' computation with an intermediate result of type 'a' and final result of type 'r' type Cont r a = (a -> r) -> r Cont is a type constructor that takes two type arguments, r and a. This means that Cont r a can always be substituted by (a -> r) -> r. For example, Cont String Int is equivalent to (Int -> String) -> String (a -> r) is the type of a function from a to r. For example, Int -> Bool is the type of a function from Int to Bool. (a -> r) -> r is the type of a function that takes a function from (a -> r) as its argument and returns an r. So Cont String Int takes a function from Int to String as its argument and finally returns a String. http://www.haskellforall.com/2012/12/the-continuation-monad.html http://www.haskellforall.com/2012/12/the-continuation-monad.... https://begriffs.com/posts/2015-06-03-haskell-continuations.html https://begriffs.com/posts/2015-06-03-haskell-continuations....
  - PopsiclePete 9y ago
    My eyes glazed over as they usually do when trying to grok Haskell, but is that somehow related to partial computation and partial functions?
    - piinbinary 9y ago
      read the right hand side as roughly: func(func(a): b): b
    - theoh 9y ago
      Not really to do with partial evaluation or the unrelated idea of a partial function. A key motivating (non-Haskell) example behind continuations is the idea of replacing "return" with a function call. This is continuation passing style, and obviously when you call a subroutine in CPS, you need to give it a function to call when it completes: a "continuation" which is contrived to be equivalent to what would happen when that particular subroutine "returned" in normal direct style
- danidiaz 9y ago
  Cont is one of the trickier monads to "get". Cont r a is a computation that knows how to produce an "a" but, instead of returning it directly, passes it to a function that takes the "a" and produces an "r". Compared to typical sequential execution, this gives more power to the "current" phase of the computation, because it might choose to invoke the passed a -> r function more than one time, none at all, inspect the resulting "r" and change course based on the result, etc.
- chriswarbo 9y ago
  > I'm reading it as 'Container' passed 'r' and 'a' performs 'a' to 'r' which returns 'r'. (I'm guessing on verbs here). This is an equation; it's a relating/defining one thing in terms of other things. In particular, there's no concept of "performing" (e.g. there's no time, state, etc. here) In this case "Cont" is just a name; we can tell that, since the equation tells us that "Cont r a" is equal to some other thing involving "r" and "a", so we could just as well use that other thing (that's what it means for two things to be equal!). Hence, "Cont r a" is just a shorthand for "(a -> r) -> r". So what is "(a -> r) -> r"? In general, for any types "x" and "y", the type "x -> y" is the type of functions which take an "x" as input and return a "y". So "a -> r" is a function which takes an "a" and returns an "r". So "(a -> r) -> r" is a function which takes a function from "a" to "r", and returns an "r".
zengid 9y ago
I know it's easy (and fun) to hate on Microsoft, but damn do they employ some great engineers/researchers: Erik Meijer, Anders Hejlsberg, Simon Peyton Jones, etc..
- redtuesday 9y ago
  Yeah, when Leslie Lamport was mentioned a few days ago I thought to myself that MS has many, many more employees that I know from reading/watching in videos compared to apple, google, ibm etc.
  - nickpsecurity 9y ago
    It's Microsoft Research, specifically, that pulls in most of this great talent. Let's not forget the VMS's people run by Cutler that made the kernel, the Xbox hypervisor, and some other stuff. Add Butler Lampson if we're talking CompSci people. The teams behind Dafny, VerveOS, Ironclad, VCC, etc are way ahead of most language-based safety or formal verification in terms of cost/benefit analysis: https://en.wikipedia.org/wiki/Butler_Lampson https://en.wikipedia.org/wiki/Butler_Lampson http://rise4fun.com/ http://rise4fun.com/
    - cwyers 9y ago
      Of the three parent listed, I think two (Meijer and Hejlsberg) were both DevDiv. Cutler was OS before moving to Xbox of all things, and I think he's at Azure now? It's certainly not only MSR hiring these guys.
      - nickpsecurity 9y ago
        I should've broken up the comment a bit as it looks like I meant all MS Research as you said. I meant to say something along the lines of (1) MS Research is doing a lot of great stuff with some examples and (2) Butler Lampson should've been on the parent's list of top talent at Microsoft. Appreciate you telling me about the mistake, though. :)
- 9y ago
lindbergh 9y ago
Erik Meijer a very engaging person! If I recall correctly, he spearheaded the Linq project for C# back in mid-2000s. In particular, I suggest his Haskell lectures to anyone interesting by theoretical aspects of functional programming. https://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Functional-Programming-Fundamentals/Lecture-Series-Erik-Meijer-Functional-Programming-Fundamentals-Chapter-1 https://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Fun...
- chubot 9y ago
  I just read over "Confessions of a used programming language salesman" [1] again. I didn't quite get it the first time around, but now I get it. Good read. It is about the road from research to production, culminating in LINQ. [1] https://scholar.google.com/scholar?cluster=17368623574878046313&hl=en&as_sdt=0,5&sciodt=0,5 https://scholar.google.com/scholar?cluster=17368623574878046...
riwsky 9y ago
In case people were wondering, the haskell stdlib answer to his interview question is at https://hackage.haskell.org/package/transformers-0.5.2.0/docs/src/Control.Monad.Trans.Cont.html#ContT https://hackage.haskell.org/package/transformers-0.5.2.0/doc... (ContT is a generalized form which lets people run, for example, computations that involve IO). Though explaining it is still the fun part.
tempodox 9y ago
> ... prove that this type forms a monad. How do I “prove” a type forms a monad? I only have to implement `lift` and `bind` with the correct behavior, and I have a monadic interface. Did I prove then that the type forms a monad?
- MarisaKirisame 9y ago
  Assuming "correct behavior" mean no bottom, and follow monad law, yes.
gumby 9y ago
While I agree with this point: > Good developers understand that they can't do everything, and they know how to leverage tools as prosthetics for their brains. it can also become a distracting fetish.

102 points by k4rtik 9y ago

Can anyone help me interpret the type signature Meijer used in his programming question? "Given a generic type: Cont r a = (a -> r) -> r Prove that this type forms a monad." I'm reading it as 'Container' passed 'r' and 'a' performs 'a' to 'r' which returns 'r'. (I'm guessing on verbs here).. I've never come across a good way to read these type signatures.

bjl 9y ago
I read this as 'A cont of type r a is a function that, given a function of type a to r, returns an r'.
hdhzy 9y ago
Cont refers to the continuation monad. For details see http://www.haskellforall.com/2012/12/the-continuation-monad.html http://www.haskellforall.com/2012/12/the-continuation-monad....
wz1000 9y ago
Cont stands for Continuation. A continuation basically represents a 'suspended' computation with an intermediate result of type 'a' and final result of type 'r' type Cont r a = (a -> r) -> r Cont is a type constructor that takes two type arguments, r and a. This means that Cont r a can always be substituted by (a -> r) -> r. For example, Cont String Int is equivalent to (Int -> String) -> String (a -> r) is the type of a function from a to r. For example, Int -> Bool is the type of a function from Int to Bool. (a -> r) -> r is the type of a function that takes a function from (a -> r) as its argument and returns an r. So Cont String Int takes a function from Int to String as its argument and finally returns a String. http://www.haskellforall.com/2012/12/the-continuation-monad.html http://www.haskellforall.com/2012/12/the-continuation-monad.... https://begriffs.com/posts/2015-06-03-haskell-continuations.html https://begriffs.com/posts/2015-06-03-haskell-continuations....
- PopsiclePete 9y ago
  My eyes glazed over as they usually do when trying to grok Haskell, but is that somehow related to partial computation and partial functions?
  - piinbinary 9y ago
    read the right hand side as roughly: func(func(a): b): b
  - theoh 9y ago
    Not really to do with partial evaluation or the unrelated idea of a partial function. A key motivating (non-Haskell) example behind continuations is the idea of replacing "return" with a function call. This is continuation passing style, and obviously when you call a subroutine in CPS, you need to give it a function to call when it completes: a "continuation" which is contrived to be equivalent to what would happen when that particular subroutine "returned" in normal direct style
danidiaz 9y ago
Cont is one of the trickier monads to "get". Cont r a is a computation that knows how to produce an "a" but, instead of returning it directly, passes it to a function that takes the "a" and produces an "r". Compared to typical sequential execution, this gives more power to the "current" phase of the computation, because it might choose to invoke the passed a -> r function more than one time, none at all, inspect the resulting "r" and change course based on the result, etc.
chriswarbo 9y ago
> I'm reading it as 'Container' passed 'r' and 'a' performs 'a' to 'r' which returns 'r'. (I'm guessing on verbs here). This is an equation; it's a relating/defining one thing in terms of other things. In particular, there's no concept of "performing" (e.g. there's no time, state, etc. here) In this case "Cont" is just a name; we can tell that, since the equation tells us that "Cont r a" is equal to some other thing involving "r" and "a", so we could just as well use that other thing (that's what it means for two things to be equal!). Hence, "Cont r a" is just a shorthand for "(a -> r) -> r". So what is "(a -> r) -> r"? In general, for any types "x" and "y", the type "x -> y" is the type of functions which take an "x" as input and return a "y". So "a -> r" is a function which takes an "a" and returns an "r". So "(a -> r) -> r" is a function which takes a function from "a" to "r", and returns an "r".

zengid 9y ago

I know it's easy (and fun) to hate on Microsoft, but damn do they employ some great engineers/researchers: Erik Meijer, Anders Hejlsberg, Simon Peyton Jones, etc..

redtuesday 9y ago
Yeah, when Leslie Lamport was mentioned a few days ago I thought to myself that MS has many, many more employees that I know from reading/watching in videos compared to apple, google, ibm etc.
- nickpsecurity 9y ago
  It's Microsoft Research, specifically, that pulls in most of this great talent. Let's not forget the VMS's people run by Cutler that made the kernel, the Xbox hypervisor, and some other stuff. Add Butler Lampson if we're talking CompSci people. The teams behind Dafny, VerveOS, Ironclad, VCC, etc are way ahead of most language-based safety or formal verification in terms of cost/benefit analysis: https://en.wikipedia.org/wiki/Butler_Lampson https://en.wikipedia.org/wiki/Butler_Lampson http://rise4fun.com/ http://rise4fun.com/
  - cwyers 9y ago
    Of the three parent listed, I think two (Meijer and Hejlsberg) were both DevDiv. Cutler was OS before moving to Xbox of all things, and I think he's at Azure now? It's certainly not only MSR hiring these guys.
    - nickpsecurity 9y ago
      I should've broken up the comment a bit as it looks like I meant all MS Research as you said. I meant to say something along the lines of (1) MS Research is doing a lot of great stuff with some examples and (2) Butler Lampson should've been on the parent's list of top talent at Microsoft. Appreciate you telling me about the mistake, though. :)
9y ago

lindbergh 9y ago

Erik Meijer a very engaging person! If I recall correctly, he spearheaded the Linq project for C# back in mid-2000s. In particular, I suggest his Haskell lectures to anyone interesting by theoretical aspects of functional programming. https://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Functional-Programming-Fundamentals/Lecture-Series-Erik-Meijer-Functional-Programming-Fundamentals-Chapter-1 https://channel9.msdn.com/Series/C9-Lectures-Erik-Meijer-Fun...

chubot 9y ago
I just read over "Confessions of a used programming language salesman" [1] again. I didn't quite get it the first time around, but now I get it. Good read. It is about the road from research to production, culminating in LINQ. [1] https://scholar.google.com/scholar?cluster=17368623574878046313&hl=en&as_sdt=0,5&sciodt=0,5 https://scholar.google.com/scholar?cluster=17368623574878046...

riwsky 9y ago

In case people were wondering, the haskell stdlib answer to his interview question is at https://hackage.haskell.org/package/transformers-0.5.2.0/docs/src/Control.Monad.Trans.Cont.html#ContT https://hackage.haskell.org/package/transformers-0.5.2.0/doc... (ContT is a generalized form which lets people run, for example, computations that involve IO). Though explaining it is still the fun part.

tempodox 9y ago

> ... prove that this type forms a monad. How do I “prove” a type forms a monad? I only have to implement `lift` and `bind` with the correct behavior, and I have a monadic interface. Did I prove then that the type forms a monad?

MarisaKirisame 9y ago
Assuming "correct behavior" mean no bottom, and follow monad law, yes.

gumby 9y ago

While I agree with this point: > Good developers understand that they can't do everything, and they know how to leverage tools as prosthetics for their brains. it can also become a distracting fetish.