This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Re: Scaladoc that is actually useful?

129 replies
ounos
Joined: 2008-12-29,
User offline. Last seen 3 years 44 weeks ago.
Re: Scaladoc that is actually useful?

Alright, I think we can finally agree and end this peacefully. The
signature *plus* some assumptions (encoded in perfectly good english)
may make it once-habitated. The scala signature itself does _not_,
since it does not by itself provide any extra assumptions. Many of us
thought perhaps misunderstood that you were saying that the latter is
also once-habitated by itself, so no english were needed in the
scaladocs - while they *are* needed to make this extra claim, thus the
debate. End of story. Is that ok with you?

2009/11/13 Tony Morris :
> Please don't be dishonest. This is the *fourth time*.
>
> Let's restate the assumptions:
>
> * Assume termination
> * No subverting the types
>
> Dimitris Andreou wrote:
>> 2009/11/13 Tony Morris :
>>
>>> Actually, I didn't claim that at all.
>>>
>>
>> Erm... "I assure you, the signature given is once-inhabited" - and you
>> kind of insisted that you were talking about scala...
>>
>>
>>> For the fourth time...
>>>
>>> ah bugger it. And no, the halting problem does not contradict that at
>>> all (ugh!).
>>>
>>
>> But you are right about that, of course. It doesn't take a halting
>> problem to prove that there are non-terminating implementations (which
>> simultaneously conform to the supposedly once-habitated signature
>> though!), one can just create a trivial example.
>>
>> Bye!
>>
>>> Dimitris Andreou wrote:
>>>
>>>> Since *you* claimed that there was only a single implementation of
>>>> that signature, it is *you* that imply that all possible
>>>> implementations are halting. Guess what, that's exactly what the
>>>> halting problem contradicts :)
>>>>
>>>> See you! It was fun :)
>>>> I really like you you know, but sometimes I think you just rant
>>>> unchecked (with no suppress compiler option :) )
>>>>
>>>> Good night all,
>>>> Dimitris
>>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> "I am not discussing this matter any further until you have solved the
>>>>> turing halting problem!"
>>>>>
>>>>> That's fine by me, I'm exhausted :) Seeya!
>>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> Omg, you used...english! Please encode these constrains as a scala
>>>>>> signature and I go home. :)
>>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>>>> a third time:
>>>>>>>
>>>>>>> * No subverting the types
>>>>>>> * Assume termination
>>>>>>>
>>>>>>> *crosses fingers*
>>>>>>>
>>>>>>> Dimitris Andreou wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>>>> see that.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>>>
>>>>>>>> This is the signature I see you gave:
>>>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>>>
>>>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>>>> signature I missed, please repeat.
>>>>>>>>
>>>>>>>> Dimitris
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>>>
>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>>>> not even a debate.
>>>>>>>>>>>
>>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>>>> aware that Scala does not have an effect system.  The question arises,
>>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>>>
>>>>>>>>>>> I will repeat myself:
>>>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>>>
>>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>>>
>>>>>>>>>>> I am exhausted, you win.
>>>>>>>>>>>
>>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> Rex,
>>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>>>
>>>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>>>
>>>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>>>
>>>>>>>>>>>> Regards,
>>>>>>>>>>>> Dimitris
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>>>> P Q P->Q
>>>>>>>>>>>>> 0 0 1
>>>>>>>>>>>>> 0 1 1
>>>>>>>>>>>>> 1 0 0
>>>>>>>>>>>>> 1 1 1
>>>>>>>>>>>>>
>>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>>>
>>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>>>
>>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>>>
>>>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> Tony,
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>>>> function.  If the return type for the Double function is not Double,
>>>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>   --Rex
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>>> > wrote:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>     You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>     I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>>>     just make
>>>>>>>>>>>>>>     it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>>>     predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>>>     interesting one.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>     Rex Kerr wrote:
>>>>>>>>>>>>>>     > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>>>     > that type signature, given that A and B can be any type.  What
>>>>>>>>>>>>>>     if foo
>>>>>>>>>>>>>>     > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>>>     leaving
>>>>>>>>>>>>>>     > everything else alone?  The type system *only says that boo gives a
>>>>>>>>>>>>>>     > function that takes A and returns C*.  It doesn't say anything about
>>>>>>>>>>>>>>     > how.  There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>>>     > might have practical utility.
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > For example,
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>>>     >   new (a:A) => (c:C) {
>>>>>>>>>>>>>>     >     val b = f(a)
>>>>>>>>>>>>>>     >     g(
>>>>>>>>>>>>>>     >       b match {
>>>>>>>>>>>>>>     >         case x:Int : -x
>>>>>>>>>>>>>>     >         case x:Long : -x
>>>>>>>>>>>>>>     >         case x:Float : -x
>>>>>>>>>>>>>>     >         case x:Double: -x
>>>>>>>>>>>>>>     >         case y: y
>>>>>>>>>>>>>>     >       }
>>>>>>>>>>>>>>     >     )
>>>>>>>>>>>>>>     >   }
>>>>>>>>>>>>>>     > }
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>>>     the idea.)
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > This is *entirely fine* by the type system.  It takes exactly
>>>>>>>>>>>>>>     what is
>>>>>>>>>>>>>>     > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>>>     what is
>>>>>>>>>>>>>>     > promised.
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>>>     one-to-one
>>>>>>>>>>>>>>     > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>>>     > handle.  (Unless, of course, you think that def
>>>>>>>>>>>>>>     > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>>>     > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>>>     > system is impractical.)
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     >   --Rex
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>>>    
>>>>>>>>>>>>>>     > >> wrote:
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     >     Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>>>     ability to
>>>>>>>>>>>>>>     >     print
>>>>>>>>>>>>>>     >     a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>>>     legacy.
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     >     There is only *one possible answer*.
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>     --
>>>>>>>>>>>>>>     Tony Morris
>>>>>>>>>>>>>>     http://tmorris.net/
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>> --
>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>> --
>>>>>>>>>>> Tony Morris
>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

The interesting part is the conclusion, once-inhabited. And the
indisputable conclusion: "it is impossible to write tests or even
documentation for this function without redundancy or error."

We could get to other cases and whether it is safe to make these
assumptions, but look how much effort it took to get this far.

Naftoli Gugenheim wrote:
> Now I'm very confused.
> So methods that don't conform to these assumptions should indeed have
> English scaladocs? Or just ScalaCheck tests? And how would one browse
> them?
>
>
> On Thu, Nov 12, 2009 at 8:04 PM, Tony Morris > wrote:
>
> Please don't be dishonest. This is the *fourth time*.
>
> Let's restate the assumptions:
>
> * Assume termination
> * No subverting the types
>
> Dimitris Andreou wrote:
> > 2009/11/13 Tony Morris >:
> >
> >> Actually, I didn't claim that at all.
> >>
> >
> > Erm... "I assure you, the signature given is once-inhabited" -
> and you
> > kind of insisted that you were talking about scala...
> >
> >
> >> For the fourth time...
> >>
> >> ah bugger it. And no, the halting problem does not contradict
> that at
> >> all (ugh!).
> >>
> >
> > But you are right about that, of course. It doesn't take a halting
> > problem to prove that there are non-terminating implementations
> (which
> > simultaneously conform to the supposedly once-habitated signature
> > though!), one can just create a trivial example.
> >
> > Bye!
> >
> >> Dimitris Andreou wrote:
> >>
> >>> Since *you* claimed that there was only a single implementation of
> >>> that signature, it is *you* that imply that all possible
> >>> implementations are halting. Guess what, that's exactly what the
> >>> halting problem contradicts :)
> >>>
> >>> See you! It was fun :)
> >>> I really like you you know, but sometimes I think you just rant
> >>> unchecked (with no suppress compiler option :) )
> >>>
> >>> Good night all,
> >>> Dimitris
> >>>
> >>> 2009/11/13 Tony Morris >:
> >>>
> >>>
> >>>> "I am not discussing this matter any further until you have
> solved the
> >>>> turing halting problem!"
> >>>>
> >>>> That's fine by me, I'm exhausted :) Seeya!
> >>>>
> >>>> Dimitris Andreou wrote:
> >>>>
> >>>>
> >>>>> Omg, you used...english! Please encode these constrains as a
> scala
> >>>>> signature and I go home. :)
> >>>>>
> >>>>> 2009/11/13 Tony Morris >:
> >>>>>
> >>>>>
> >>>>>
> >>>>>> You seem to have overlooked some important parts. I will
> repeat them for
> >>>>>> a third time:
> >>>>>>
> >>>>>> * No subverting the types
> >>>>>> * Assume termination
> >>>>>>
> >>>>>> *crosses fingers*
> >>>>>>
> >>>>>> Dimitris Andreou wrote:
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>> 2009/11/13 Tony Morris >:
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>> I did. I'm not sure what to do about the fact that you
> have failed to
> >>>>>>>> see that.
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>> I hope that was *not* your favourite line as a lecturer :)
> >>>>>>>
> >>>>>>> This is the signature I see you gave:
> >>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
> >>>>>>>
> >>>>>>> It does not constrain "boo" (scala) implementations from
> using the
> >>>>>>> implicit world. So you did not address my request. If you
> gave another
> >>>>>>> signature I missed, please repeat.
> >>>>>>>
> >>>>>>> Dimitris
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>> Dimitris Andreou wrote:
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>> As I said, please give us a scala signature that
> constrains its body
> >>>>>>>>> from not using the world. Otherwise, I would be very
> happy to see how
> >>>>>>>>> exactly you encode the mathematical signature into a
> scala signature
> >>>>>>>>> which also has just one implementation. Thank you.
> >>>>>>>>>
> >>>>>>>>> 2009/11/13 Tony Morris >:
> >>>>>>>>>
> >>>>>>>>>
> >>>>>>>>>
> >>>>>>>>>
> >>>>>>>>>
> >>>>>>>>>> It's entirely possible to construct a de-facto world
> state. The
> >>>>>>>>>> signature definitely does have just one instance. It
> definitely does.
> >>>>>>>>>> There is a proof. The strongest possible claim about
> reality exists.
> >>>>>>>>>> There's not much I can do about the fact that you are
> refuting a proof
> >>>>>>>>>> by simply asserting the contrary. I'd move this to
> scala-debate but it's
> >>>>>>>>>> not even a debate.
> >>>>>>>>>>
> >>>>>>>>>> I talk about *functions* and definitely Scala
> programming. I'm well
> >>>>>>>>>> aware that Scala does not have an effect system. The
> question arises,
> >>>>>>>>>> what shall we do about it? The answer is not English.
> Rex hasn't already
> >>>>>>>>>> made this point -- *I* have already made this point.
> >>>>>>>>>>
> >>>>>>>>>> I will repeat myself:
> >>>>>>>>>> (A => B) => (B => C) => A => C
> >>>>>>>>>>
> >>>>>>>>>> No subverting the types, assume termination -->
> once-inhabited!
> >>>>>>>>>>
> >>>>>>>>>> I am exhausted, you win.
> >>>>>>>>>>
> >>>>>>>>>> Dimitris Andreou wrote:
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>> 2009/11/13 Tony Morris >:
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>> Rex,
> >>>>>>>>>>>> I can read your code just fine. I assure you, the
> signature given is
> >>>>>>>>>>>> once-inhabited. There is even a proof of this fact.
> It's a well
> >>>>>>>>>>>> understood basic fact of computational theory.
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>> The problem is that a signature never captures the
> implicit "world"
> >>>>>>>>>>> argument that all functions have (otherwise, please
> show me your
> >>>>>>>>>>> functions having the "world" argument from which you
> access all of
> >>>>>>>>>>> scala libraries) . So the signature definitely has
> *not* just one
> >>>>>>>>>>> instance, but infinitely many.
> >>>>>>>>>>>
> >>>>>>>>>>> If you don't assume that a function is able to compute
> other
> >>>>>>>>>>> functions, just because it didn't have them as
> arguments, you talk
> >>>>>>>>>>> about something else but definitely not about scala
> programming. May I
> >>>>>>>>>>> remind that the discussion is about _scala_ docs.
> >>>>>>>>>>>
> >>>>>>>>>>> This point has already been made by Rex but lets try
> it again :)
> >>>>>>>>>>>
> >>>>>>>>>>> Regards,
> >>>>>>>>>>> Dimitris
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>> So, the question arises, where are you wrong? The
> theorem: forall A B. A
> >>>>>>>>>>>> -> B is also known as "the cast operator." Under the
> Curry-Howard
> >>>>>>>>>>>> Isomorphism, functions are implication -- that is why
> we denote them
> >>>>>>>>>>>> with -> symbol.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Let's draw the truth table for implication:
> >>>>>>>>>>>> P Q P->Q
> >>>>>>>>>>>> 0 0 1
> >>>>>>>>>>>> 0 1 1
> >>>>>>>>>>>> 1 0 0
> >>>>>>>>>>>> 1 1 1
> >>>>>>>>>>>>
> >>>>>>>>>>>> So we have a premise and a conclusion in one. We see
> immediately that
> >>>>>>>>>>>> this is not tautological. Therefore, forall A B. A ->
> B is not a
> >>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting
> Erik Meijer at a
> >>>>>>>>>>>> conference in front about ~400 typical programmers,
> "It is a LIE!"
> >>>>>>>>>>>>
> >>>>>>>>>>>> Scala's type systems has many "let's escape reality
> and tell lies." One
> >>>>>>>>>>>> of them is side-effects, another is casting. Haskell,
> which also does
> >>>>>>>>>>>> same, calls the former unsafePerformIO and the latter
> unsafeCoerce. The
> >>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these
> functions tell lies."
> >>>>>>>>>>>>
> >>>>>>>>>>>> The question can be phrased in English as "tell the
> truth about this
> >>>>>>>>>>>> signature." This means no lies, no subverting the
> types. No def cast[A,
> >>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you
> use them is the
> >>>>>>>>>>>> extent that you are telling lies (and so we must not
> get *all* our
> >>>>>>>>>>>> documentation from types, but we should strive for it
> as a virtue).
> >>>>>>>>>>>>
> >>>>>>>>>>>> I really hope this helps. This is exhausting.
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>> Rex Kerr wrote:
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>> Tony,
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> I'm not convinced you're paying attention to my
> code, and if you are,
> >>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> Please explain exactly where the subversion occurs,
> and please say
> >>>>>>>>>>>>> exactly what the return type should be for the
> Double square
> >>>>>>>>>>>>> function. If the return type for the Double
> function is not Double,
> >>>>>>>>>>>>> please explain what the return type is for the F(n)
> function which
> >>>>>>>>>>>>> computes the n'th Fibonacci number.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> Or you can come up with some alternate scheme that
> will demonstrate
> >>>>>>>>>>>>> that you are actually understanding what I am saying
> and disagreeing
> >>>>>>>>>>>>> on the basis of solid principles.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> (Or, of course, we can just drop it.)
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> --Rex
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris
>
> >>>>>>>>>>>>> >> wrote:
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> You've subverted the types again. forall A B. A
> -> B is not a theorem.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> I assure you, there is only one possible
> solution and I didn't
> >>>>>>>>>>>>> just make
> >>>>>>>>>>>>> it up. I refer back to my lobbying for basic
> type theory in schools. I
> >>>>>>>>>>>>> predict we wouldn't be having this discussion,
> but a more
> >>>>>>>>>>>>> interesting one.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> Rex Kerr wrote:
> >>>>>>>>>>>>> > There are infinitely many possible answers to
> what can happen with
> >>>>>>>>>>>>> > that type signature, given that A and B can be
> any type. What
> >>>>>>>>>>>>> if foo
> >>>>>>>>>>>>> > picks out certain Bs and converts them to
> different B's, while
> >>>>>>>>>>>>> leaving
> >>>>>>>>>>>>> > everything else alone? The type system *only
> says that boo gives a
> >>>>>>>>>>>>> > function that takes A and returns C*. It
> doesn't say anything about
> >>>>>>>>>>>>> > how. There's an obvious path, and lots of
> non-obvious paths that
> >>>>>>>>>>>>> > might have practical utility.
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > For example,
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
> >>>>>>>>>>>>> > new (a:A) => (c:C) {
> >>>>>>>>>>>>> > val b = f(a)
> >>>>>>>>>>>>> > g(
> >>>>>>>>>>>>> > b match {
> >>>>>>>>>>>>> > case x:Int : -x
> >>>>>>>>>>>>> > case x:Long : -x
> >>>>>>>>>>>>> > case x:Float : -x
> >>>>>>>>>>>>> > case x:Double: -x
> >>>>>>>>>>>>> > case y: y
> >>>>>>>>>>>>> > }
> >>>>>>>>>>>>> > )
> >>>>>>>>>>>>> > }
> >>>>>>>>>>>>> > }
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > (I didn't run this, so there may be syntax
> errors, but you get
> >>>>>>>>>>>>> the idea.)
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > This is *entirely fine* by the type system.
> It takes exactly
> >>>>>>>>>>>>> what is
> >>>>>>>>>>>>> > promised, has no side effects whatsoever, and
> returns exactly
> >>>>>>>>>>>>> what is
> >>>>>>>>>>>>> > promised.
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > Sure, there are now some subset of inputs that
> may have had
> >>>>>>>>>>>>> one-to-one
> >>>>>>>>>>>>> > mappings that now are not, but that's not the
> type system's job to
> >>>>>>>>>>>>> > handle. (Unless, of course, you think that def
> >>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the
> proper type signature for
> >>>>>>>>>>>>> > the x*x operation; in that case, I'd just
> point out that such a type
> >>>>>>>>>>>>> > system is impractical.)
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > --Rex
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > >>> wrote:
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > Unfortunately you have subverted the
> types. There is no
> >>>>>>>>>>>>> ability to
> >>>>>>>>>>>>> > print
> >>>>>>>>>>>>> > a universal type. This is an unfortunate
> part of the Java
> >>>>>>>>>>>>> legacy.
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> > There is only *one possible answer*.
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>> >
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> --
> >>>>>>>>>>>>> Tony Morris
> >>>>>>>>>>>>> http://tmorris.net/
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>> --
> >>>>>>>>>>>> Tony Morris
> >>>>>>>>>>>> http://tmorris.net/
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>> --
> >>>>>>>>>> Tony Morris
> >>>>>>>>>> http://tmorris.net/
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>> --
> >>>>>>>> Tony Morris
> >>>>>>>> http://tmorris.net/
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>>>>
> >>>>>> --
> >>>>>> Tony Morris
> >>>>>> http://tmorris.net/
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>> --
> >>>> Tony Morris
> >>>> http://tmorris.net/
> >>>>
> >>>>
> >>>>
> >>>>
> >>>>
> >>>
> >> --
> >> Tony Morris
> >> http://tmorris.net/
> >>
> >>
> >>
> >>
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

Brian, you're a saviour. Thanks for taking something interesting from
this exhaustive discussion.

There are other interesting facts to be made from here too! I only gave
a trivial and easy to prove (haha!) case for the purpose of discussing
Scaladoc.

Someone else (nameless for now) found it "interesting" that it was even
a discussion worth having, and felt it most appropriate to simply
conclude (see free theorems):
> @free cmp :: (b -> c) -> (a -> b) -> (a -> c)
> g . k = p . f => f . q = f1 . h => g . cmp k q = cmp p f1 . h

Brian Maso wrote:
> Well, I think we understand how there is only one definition of
> def func[A, B, C](f1: A=>B, f2: B=>C): A=>C
>
> when there are no constraints on A, B, or C, and where no implicit
> values or contextual (imported) values are used in the body of the
> function. That is, for *all* A, B and C (as opposed to for *some* A, B
> and C, which is how I had misread the original). That's actually
> mildly interesting. Not sure how I'm going to use that in the future,
> or the rest of Types as Theories, to build webpages faster... Now
> *that* would be a great college course!
>
> Best regards,
> Brian Maso
> (949) 395-8551
> brian [at] blumenfeld-maso [dot] com
> twitter: @bmaso
> skype: brian.maso
> LinkedIn: http://www.linkedin.com/in/brianmaso
>
>
> On Thu, Nov 12, 2009 at 5:03 PM, Tony Morris > wrote:
>
> I didn't say that the type signature was all that you needed. I gave a
> specific case. It is a fact that, were it not also lamentable, would
> also be somewhat amusing that this is causing a "debate."
>
> If you wish to understand why => means implication and why Either
> means
> disjunction and why Tuple2 means conjunction and ..., then I
> direct you
> to any introduction to the Curry-Howard isomorphism, also known as
> (wait
> for it!), Types as Theorems.
>
> There is also a great paper out there on what is commonly called Free
> Theorems.
>
> I am too exhausted to pursue this matter. I was hoping for a different
> outcome. Hopefully the silent audience did some thinking!
>
> christopher marshall wrote:
> > How does a function:
> >
> > def foo(i: Int) : String
> >
> > Tell me anything about what the function *actually does*, regardless
> > of whether, under some given definition of "implies" the
> statement Int
> > => String is "true", given foo. I must be completely missing some
> > point here because for the life of me I don't really understand the
> > train of thought that says that the type signature of a function is
> > all you need to parse to understand what the function does.
> >
> > > Date: Fri, 13 Nov 2009 10:31:34 +1000
> > > From: tonymorris [at] gmail [dot] com
> > > To: oxbow_lakes [at] hotmail [dot] com
> > > CC: jim [dot] andreou [at] gmail [dot] com ;
> ichoran [at] gmail [dot] com ;
> scala-user [at] listes [dot] epfl [dot] ch
> > > Subject: Re: [scala-user] Scaladoc that is actually useful?
> > >
> > >
> > >
> > > christopher marshall wrote:
> > > > The fact that you are using => to mean the mathematical/logic
> > > > "implies" seems to ignore the fact that in Scala, => means
> no such
> > > > thing. A, B and C are not statements/sentences: in a scala
> signature,
> > > > they are types and the signature tells me nothing about what the
> > > > method/function actually does! *Why are we even arguing
> about this?*
> > >
> > > Actually, in Scala it means exactly that. Please see the C-H
> > Isomorphism.
> > >
> > > --
> > > Tony Morris
> > > http://tmorris.net/
> > >
> > >
> >
> >
> ------------------------------------------------------------------------
> > Use Hotmail to send and receive mail from your different email
> > accounts. Find out how.
>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:
> Still need some language (e.g. english) to describe these
> assumptions. They are not axioms you know or theorems, they
> are...argh...assumptions. Please document your assumptions! Please
> ask students to document their assumptions :)

That is precisely what they are, axioms.

Randall Schulz

ounos
Joined: 2008-12-29,
User offline. Last seen 3 years 44 weeks ago.
Re: Scaladoc that is actually useful?

2009/11/13 Tony Morris :
> Actually, I didn't claim that at all.

Erm... "I assure you, the signature given is once-inhabited" - and you
kind of insisted that you were talking about scala...

>
> For the fourth time...
>
> ah bugger it. And no, the halting problem does not contradict that at
> all (ugh!).

But you are right about that, of course. It doesn't take a halting
problem to prove that there are non-terminating implementations (which
simultaneously conform to the supposedly once-habitated signature
though!), one can just create a trivial example.

Bye!
>
> Dimitris Andreou wrote:
>> Since *you* claimed that there was only a single implementation of
>> that signature, it is *you* that imply that all possible
>> implementations are halting. Guess what, that's exactly what the
>> halting problem contradicts :)
>>
>> See you! It was fun :)
>> I really like you you know, but sometimes I think you just rant
>> unchecked (with no suppress compiler option :) )
>>
>> Good night all,
>> Dimitris
>>
>> 2009/11/13 Tony Morris :
>>
>>> "I am not discussing this matter any further until you have solved the
>>> turing halting problem!"
>>>
>>> That's fine by me, I'm exhausted :) Seeya!
>>>
>>> Dimitris Andreou wrote:
>>>
>>>> Omg, you used...english! Please encode these constrains as a scala
>>>> signature and I go home. :)
>>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>> a third time:
>>>>>
>>>>> * No subverting the types
>>>>> * Assume termination
>>>>>
>>>>> *crosses fingers*
>>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>> see that.
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>
>>>>>> This is the signature I see you gave:
>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>
>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>> signature I missed, please repeat.
>>>>>>
>>>>>> Dimitris
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>> Dimitris Andreou wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>
>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>> not even a debate.
>>>>>>>>>
>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>> aware that Scala does not have an effect system.  The question arises,
>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>
>>>>>>>>> I will repeat myself:
>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>
>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>
>>>>>>>>> I am exhausted, you win.
>>>>>>>>>
>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> Rex,
>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>
>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>
>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>
>>>>>>>>>> Regards,
>>>>>>>>>> Dimitris
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>
>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>> P Q P->Q
>>>>>>>>>>> 0 0 1
>>>>>>>>>>> 0 1 1
>>>>>>>>>>> 1 0 0
>>>>>>>>>>> 1 1 1
>>>>>>>>>>>
>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>
>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>
>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>
>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> Tony,
>>>>>>>>>>>>
>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>
>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>> function.  If the return type for the Double function is not Double,
>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>
>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>
>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>
>>>>>>>>>>>>   --Rex
>>>>>>>>>>>>
>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>> > wrote:
>>>>>>>>>>>>
>>>>>>>>>>>>     You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>
>>>>>>>>>>>>     I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>     just make
>>>>>>>>>>>>     it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>     predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>     interesting one.
>>>>>>>>>>>>
>>>>>>>>>>>>     Rex Kerr wrote:
>>>>>>>>>>>>     > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>     > that type signature, given that A and B can be any type.  What
>>>>>>>>>>>>     if foo
>>>>>>>>>>>>     > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>     leaving
>>>>>>>>>>>>     > everything else alone?  The type system *only says that boo gives a
>>>>>>>>>>>>     > function that takes A and returns C*.  It doesn't say anything about
>>>>>>>>>>>>     > how.  There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>     > might have practical utility.
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > For example,
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>     >   new (a:A) => (c:C) {
>>>>>>>>>>>>     >     val b = f(a)
>>>>>>>>>>>>     >     g(
>>>>>>>>>>>>     >       b match {
>>>>>>>>>>>>     >         case x:Int : -x
>>>>>>>>>>>>     >         case x:Long : -x
>>>>>>>>>>>>     >         case x:Float : -x
>>>>>>>>>>>>     >         case x:Double: -x
>>>>>>>>>>>>     >         case y: y
>>>>>>>>>>>>     >       }
>>>>>>>>>>>>     >     )
>>>>>>>>>>>>     >   }
>>>>>>>>>>>>     > }
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>     the idea.)
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > This is *entirely fine* by the type system.  It takes exactly
>>>>>>>>>>>>     what is
>>>>>>>>>>>>     > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>     what is
>>>>>>>>>>>>     > promised.
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>     one-to-one
>>>>>>>>>>>>     > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>     > handle.  (Unless, of course, you think that def
>>>>>>>>>>>>     > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>     > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>     > system is impractical.)
>>>>>>>>>>>>     >
>>>>>>>>>>>>     >   --Rex
>>>>>>>>>>>>     >
>>>>>>>>>>>>     > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>    
>>>>>>>>>>>>     > >> wrote:
>>>>>>>>>>>>     >
>>>>>>>>>>>>     >     Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>     ability to
>>>>>>>>>>>>     >     print
>>>>>>>>>>>>     >     a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>     legacy.
>>>>>>>>>>>>     >
>>>>>>>>>>>>     >     There is only *one possible answer*.
>>>>>>>>>>>>     >
>>>>>>>>>>>>     >
>>>>>>>>>>>>
>>>>>>>>>>>>     --
>>>>>>>>>>>>     Tony Morris
>>>>>>>>>>>>     http://tmorris.net/
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>> --
>>>>>>>>>>> Tony Morris
>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

ounos
Joined: 2008-12-29,
User offline. Last seen 3 years 44 weeks ago.
Re: Scaladoc that is actually useful?

Still need some language (e.g. english) to describe these assumptions.
They are not axioms you know or theorems, they
are...argh...assumptions. Please document your assumptions! Please ask
students to document their assumptions :)

2009/11/13 Tony Morris :
> No, the existence of these assumptions (finally!) does not justify the
> use of English for the general case.
>
> Dimitris Andreou wrote:
>> Alright, I think we can finally agree and end this peacefully. The
>> signature *plus* some assumptions (encoded in perfectly good english)
>> may make it once-habitated. The scala signature itself does _not_,
>> since it does not by itself provide any extra assumptions. Many of us
>> thought perhaps misunderstood that you were saying that the latter is
>> also once-habitated by itself, so no english were needed in the
>> scaladocs - while they *are* needed to make this extra claim, thus the
>> debate. End of story. Is that ok with you?
>>
>> 2009/11/13 Tony Morris :
>>
>>> Please don't be dishonest. This is the *fourth time*.
>>>
>>> Let's restate the assumptions:
>>>
>>> * Assume termination
>>> * No subverting the types
>>>
>>> Dimitris Andreou wrote:
>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> Actually, I didn't claim that at all.
>>>>>
>>>>>
>>>> Erm... "I assure you, the signature given is once-inhabited" - and you
>>>> kind of insisted that you were talking about scala...
>>>>
>>>>
>>>>
>>>>> For the fourth time...
>>>>>
>>>>> ah bugger it. And no, the halting problem does not contradict that at
>>>>> all (ugh!).
>>>>>
>>>>>
>>>> But you are right about that, of course. It doesn't take a halting
>>>> problem to prove that there are non-terminating implementations (which
>>>> simultaneously conform to the supposedly once-habitated signature
>>>> though!), one can just create a trivial example.
>>>>
>>>> Bye!
>>>>
>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> Since *you* claimed that there was only a single implementation of
>>>>>> that signature, it is *you* that imply that all possible
>>>>>> implementations are halting. Guess what, that's exactly what the
>>>>>> halting problem contradicts :)
>>>>>>
>>>>>> See you! It was fun :)
>>>>>> I really like you you know, but sometimes I think you just rant
>>>>>> unchecked (with no suppress compiler option :) )
>>>>>>
>>>>>> Good night all,
>>>>>> Dimitris
>>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> "I am not discussing this matter any further until you have solved the
>>>>>>> turing halting problem!"
>>>>>>>
>>>>>>> That's fine by me, I'm exhausted :) Seeya!
>>>>>>>
>>>>>>> Dimitris Andreou wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> Omg, you used...english! Please encode these constrains as a scala
>>>>>>>> signature and I go home. :)
>>>>>>>>
>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>>>>>> a third time:
>>>>>>>>>
>>>>>>>>> * No subverting the types
>>>>>>>>> * Assume termination
>>>>>>>>>
>>>>>>>>> *crosses fingers*
>>>>>>>>>
>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>>>>>> see that.
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>>>>>
>>>>>>>>>> This is the signature I see you gave:
>>>>>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>>>>>
>>>>>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>>>>>> signature I missed, please repeat.
>>>>>>>>>>
>>>>>>>>>> Dimitris
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>>>>>
>>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>>>>>> not even a debate.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>>>>>> aware that Scala does not have an effect system.  The question arises,
>>>>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I will repeat myself:
>>>>>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>>>>>
>>>>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>>>>>
>>>>>>>>>>>>> I am exhausted, you win.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Rex,
>>>>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Regards,
>>>>>>>>>>>>>> Dimitris
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>>>>>> P Q P->Q
>>>>>>>>>>>>>>> 0 0 1
>>>>>>>>>>>>>>> 0 1 1
>>>>>>>>>>>>>>> 1 0 0
>>>>>>>>>>>>>>> 1 1 1
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Tony,
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>>>>>> function.  If the return type for the Double function is not Double,
>>>>>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>   --Rex
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>>>>> > wrote:
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>     You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>     I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>>>>>     just make
>>>>>>>>>>>>>>>>     it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>>>>>     predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>>>>>     interesting one.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>     Rex Kerr wrote:
>>>>>>>>>>>>>>>>     > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>>>>>     > that type signature, given that A and B can be any type.  What
>>>>>>>>>>>>>>>>     if foo
>>>>>>>>>>>>>>>>     > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>>>>>     leaving
>>>>>>>>>>>>>>>>     > everything else alone?  The type system *only says that boo gives a
>>>>>>>>>>>>>>>>     > function that takes A and returns C*.  It doesn't say anything about
>>>>>>>>>>>>>>>>     > how.  There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>>>>>     > might have practical utility.
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > For example,
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>>>>>     >   new (a:A) => (c:C) {
>>>>>>>>>>>>>>>>     >     val b = f(a)
>>>>>>>>>>>>>>>>     >     g(
>>>>>>>>>>>>>>>>     >       b match {
>>>>>>>>>>>>>>>>     >         case x:Int : -x
>>>>>>>>>>>>>>>>     >         case x:Long : -x
>>>>>>>>>>>>>>>>     >         case x:Float : -x
>>>>>>>>>>>>>>>>     >         case x:Double: -x
>>>>>>>>>>>>>>>>     >         case y: y
>>>>>>>>>>>>>>>>     >       }
>>>>>>>>>>>>>>>>     >     )
>>>>>>>>>>>>>>>>     >   }
>>>>>>>>>>>>>>>>     > }
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>>>>>     the idea.)
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > This is *entirely fine* by the type system.  It takes exactly
>>>>>>>>>>>>>>>>     what is
>>>>>>>>>>>>>>>>     > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>>>>>     what is
>>>>>>>>>>>>>>>>     > promised.
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>>>>>     one-to-one
>>>>>>>>>>>>>>>>     > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>>>>>     > handle.  (Unless, of course, you think that def
>>>>>>>>>>>>>>>>     > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>>>>>     > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>>>>>     > system is impractical.)
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     >   --Rex
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>>>>>    
>>>>>>>>>>>>>>>>     > >> wrote:
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     >     Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>>>>>     ability to
>>>>>>>>>>>>>>>>     >     print
>>>>>>>>>>>>>>>>     >     a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>>>>>     legacy.
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     >     There is only *one possible answer*.
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>     >
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>     --
>>>>>>>>>>>>>>>>     Tony Morris
>>>>>>>>>>>>>>>>     http://tmorris.net/
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> --
>>>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>> --
>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>> --
>>>>>>>>>>> Tony Morris
>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:
> Termination is an axiom? :-/

No. The properties of a function and of the type system are axioms.

Randall Schulz

bmaso
Joined: 2009-10-04,
User offline. Last seen 2 years 40 weeks ago.
Re: Scaladoc that is actually useful?
Well, I think we understand how there is only one definition of
  def func[A, B, C](f1: A=>B, f2: B=>C): A=>C

when there are no constraints on A, B, or C, and where no implicit values or contextual (imported) values are used in the body of the function. That is, for *all* A, B and C (as opposed to for *some* A, B and C, which is how I had misread the original). That's actually mildly interesting. Not sure how I'm going to use that in the future, or the rest of Types as Theories, to build webpages faster... Now *that* would be a great college course!

Best regards,
Brian Maso
(949) 395-8551
brian [at] blumenfeld-maso [dot] com
twitter: @bmaso
skype: brian.maso
LinkedIn: http://www.linkedin.com/in/brianmaso


On Thu, Nov 12, 2009 at 5:03 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
I didn't say that the type signature was all that you needed. I gave a
specific case. It is a fact that, were it not also lamentable, would
also be somewhat amusing that this is causing a "debate."

If you wish to understand why => means implication and why Either means
disjunction and why Tuple2 means conjunction and ..., then I direct you
to any introduction to the Curry-Howard isomorphism, also known as (wait
for it!), Types as Theorems.

There is also a great paper out there on what is commonly called Free
Theorems.

I am too exhausted to pursue this matter. I was hoping for a different
outcome. Hopefully the silent audience did some thinking!

christopher marshall wrote:
> How does a function:
>
>    def foo(i: Int) : String
>
> Tell me anything about what the function *actually does*, regardless
> of whether, under some given definition of "implies" the statement Int
> => String is "true", given foo. I must be completely missing some
> point here because for the life of me I don't really understand the
> train of thought that says that the type signature of a function is
> all you need to parse to understand what the function does.
>
> > Date: Fri, 13 Nov 2009 10:31:34 +1000
> > From: tonymorris [at] gmail [dot] com
> > To: oxbow_lakes [at] hotmail [dot] com
> > CC: jim [dot] andreou [at] gmail [dot] com; ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch
> > Subject: Re: [scala-user] Scaladoc that is actually useful?
> >
> >
> >
> > christopher marshall wrote:
> > > The fact that you are using => to mean the mathematical/logic
> > > "implies" seems to ignore the fact that in Scala, => means no such
> > > thing. A, B and C are not statements/sentences: in a scala signature,
> > > they are types and the signature tells me nothing about what the
> > > method/function actually does! *Why are we even arguing about this?*
> >
> > Actually, in Scala it means exactly that. Please see the C-H
> Isomorphism.
> >
> > --
> > Tony Morris
> > http://tmorris.net/
> >
> >
>
> ------------------------------------------------------------------------
> Use Hotmail to send and receive mail from your different email
> accounts. Find out how. <http://clk.atdmt.com/UKM/go/186394592/direct/01/>

--
Tony Morris
http://tmorris.net/



Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?
Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:
> Not in scala functions/signatures though, that was the confusion of
> all this debate :) anyway, not to create a mini-private-debate. I'm
> out, good night!

You have to realize that when a method computes something at odds with
its signature, that method is buggy.

Randall Schulz

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 7:25 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
Functions are self-contained and pure. They know not of the world, other
than that portion of the world of mathematics that defines them.

Aha.  I think this is the key aspect of the idea of "function" that I was missing.

In this case, yes, I agree, if functions that take 1-ary functions as arguments may only apply operations that are valid on the set of all 1-ary functions (and that operation happens to be composition, and you may not inspect the arguments or outputs to see if they themselves happen to be in the set of all 1-ary functions so you can't do anything there either), there is only one possible thing to do: compose the functions.

I suppose that this type of property has nice consequences for provability of correctness of  programs under some limited situations.

It seems highly impractical, however, from a code duplication standpoint to never allow a generic function to understand something about the types that are thrown at it.  So, yes, nice elegance, yay, but if I am going to program something, I don't want to have to write my composition function over again _in its entirety_ for Int, Float, Double, Long, whatever, just so that I keep the type signature conforming to the "functions only import the mathematics of their arguments" rule.
 
Programmers have repeatedly been guilty of butchering established
concepts and terminology. Calling something a function that does not
conform to the definition of function universally agreed upon by
mathematicians is inexcusable.

This is absolutely not the definition of function "universally agreed upon by mathematicians".

For example,

f(x) : R -> R = {
  x == 0 : 0
  x in Z : 1/x
  else: x
}

is a perfectly well-defined function on the reals, and it knows all about integers which is disallowed by the "pure" function definition above.

The universal definition of function is, in mathematics, something very much like this:

A (single-valued) _function_ from set A to set B is a rule that specifies for any element a in A an element b in B; we call this element in B f(a).

It says nothing about how it does this.  It says nothing about whether it knows about real numbers even though its arguments are perhaps functions.  It just says it maps anything in the input set to some element of the output set.

The mathematical definition does not admit side-effects, as it is simply a mapping.  But it does not forbid _any_ method of transforming input to output.

So I submit that whatever it is that Tony defined is not actually just a function but is something more strict (perhaps a "pure function", a subset of the set of all valid functions from the described input set to the described output set).  I agree that a "function" that has side-effects is not a function in the mathematical sense, except inasmuch as it takes the world as an implicit argument and gives it as an implicit return value.

  --Rex

Dave Griffith
Joined: 2009-01-14,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

Tony Morris-4 wrote:
>
> Do you know what function means?
>

In type theory? In intuitionistic (a.k.a constructive) type theory? In
recursive function theory? In Haskell? In Scala? In C?

Yes, I know what 'function' means, in all of the above. Even though the
definitions there have almost as many differences as similarities.

In "reality"? Oh, hell no! I certainly don't know what a function is in
"reality", but based on the disagreement on this point among philosophers of
mathematics I'm pretty sure I'm not alone. The one thing I am sure of is
that it's not the sort of naive Platonism you seem to be espousing. If I
take a rock and sift it down to constituent quarks I'm pretty certain I
won't see any functions.

How exactly is this helpful to someone who is trying to get some work done
and complaining that someone else didn't write good doc?

--Dave Griffith

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

So er, back to reality.

Can you provide two inhabitants for:
forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

(Hint: the answer begins with 'n' and ends with 'o').

Dave Griffith wrote:
>
>
> Tony Morris-4 wrote:
>
>> Do you know what function means?
>>
>>
>
> In type theory? In intuitionistic (a.k.a constructive) type theory? In
> recursive function theory? In Haskell? In Scala? In C?
>
> Yes, I know what 'function' means, in all of the above. Even though the
> definitions there have almost as many differences as similarities.
>
> In "reality"? Oh, hell no! I certainly don't know what a function is in
> "reality", but based on the disagreement on this point among philosophers of
> mathematics I'm pretty sure I'm not alone. The one thing I am sure of is
> that it's not the sort of naive Platonism you seem to be espousing. If I
> take a rock and sift it down to constituent quarks I'm pretty certain I
> won't see any functions.
>
> How exactly is this helpful to someone who is trying to get some work done
> and complaining that someone else didn't write good doc?
>
> --Dave Griffith
>
>

Ishaaq Chandy
Joined: 2009-02-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?
Tony, I think you've quite adequately put the point across that

(A => B) => (B => C) => A => C

has only one truthful inhabitant and should quite legitimately be left undocumented. It could be argued that it is the onus of a programmer who writes an untruthful implementation of that function to document it instead of asking that the truthful one be documented.

Yet, I think this function has been raised as a straw-man. A large percentage of function signatures don't have the luxury of having only one inhabitant. I haven't really sat down and counted the number of such functions in the scala library that have not been documented. Nor have I counted the number side-affecting *methods* (as opposed to real functions) in the scala library that are undocumented, but my conjecture (happy for it to be proved wrong) is that those numbers are large enough to be concerned about. Which is what, IMO, the OP was concerned about.

Surely, you're not claiming that the latter two cases should not be documented?

Ishaaq

2009/11/13 Tony Morris <tonymorris [at] gmail [dot] com>
So er, back to reality.

Can you provide two inhabitants for:
forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

(Hint: the answer begins with 'n' and ends with 'o').

Dave Griffith wrote:
>
>
> Tony Morris-4 wrote:
>
>> Do you know what function means?
>>
>>
>
> In type theory?  In intuitionistic (a.k.a constructive) type theory? In
> recursive function theory?  In Haskell? In Scala? In C?
>
> Yes, I know what 'function' means, in all of the above.  Even though the
> definitions there have almost as many differences as similarities.
>
> In "reality"?  Oh, hell no!  I certainly don't know what a function is in
> "reality", but based on the disagreement on this point among philosophers of
> mathematics I'm pretty sure I'm not alone.  The one thing I am sure of is
> that it's not the sort of naive Platonism you seem to be espousing.  If I
> take a rock and sift it down to constituent quarks I'm pretty certain I
> won't see any functions.
>
> How exactly is this helpful to someone who is trying to get some work done
> and complaining that someone else didn't write good doc?
>
> --Dave Griffith
>
>

--
Tony Morris
http://tmorris.net/



Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

Hello Ishaaq,
If I have adequately conveyed a point that is provable, has been proven
(by parametricity) and is easily falsifiable, then you'd think I'd hit
less resistance., but alas, it appears not.

I think I have adequately answered your concluding question too, don't
you? For those signatures that are inhabited more than once (and yes,
there are a lot), what should we do? The rash conclusion of "write
English" is just that, rash and has about as much thought put into it as
many of the respondents have put into my original question (hence, the
laborious repetition). My answer has thus far been, "No I am not (yet)
claiming anything about function signatures with multiple inhabitants."

I haven't even got to the point of being able to examine your question
further -- instead, we are going over and over on a matter of fact as if
it is even debatable! I was hoping that once this observation was made
(that there exists a signature for which documentation/tests are
redundant), then we could raise further questions. Ah, the Scala
community :)

It has been suggested to me by two peers that I should "bash them over
the head" but I still hold hope for a productive outcome!

Ishaaq Chandy wrote:
> Tony, I think you've quite adequately put the point across that
>
> (A => B) => (B => C) => A => C
>
> has only one truthful inhabitant and should quite legitimately be left
> undocumented. It could be argued that it is the onus of a programmer
> who writes an untruthful implementation of that function to document
> it instead of asking that the truthful one be documented.
>
> Yet, I think this function has been raised as a straw-man. A large
> percentage of function signatures don't have the luxury of having only
> one inhabitant. I haven't really sat down and counted the number of
> such functions in the scala library that have not been documented. Nor
> have I counted the number side-affecting *methods* (as opposed to real
> functions) in the scala library that are undocumented, but my
> conjecture (happy for it to be proved wrong) is that those numbers are
> large enough to be concerned about. Which is what, IMO, the OP was
> concerned about.
>
> Surely, you're not claiming that the latter two cases should not be
> documented?
>
> Ishaaq
>
> 2009/11/13 Tony Morris >
>
> So er, back to reality.
>
> Can you provide two inhabitants for:
> forall A B C. (A => B) => (B => C) => A => C
>
> Assume termination and no lies.
>
> (Hint: the answer begins with 'n' and ends with 'o').
>
> Dave Griffith wrote:
> >
> >
> > Tony Morris-4 wrote:
> >
> >> Do you know what function means?
> >>
> >>
> >
> > In type theory? In intuitionistic (a.k.a constructive) type
> theory? In
> > recursive function theory? In Haskell? In Scala? In C?
> >
> > Yes, I know what 'function' means, in all of the above. Even
> though the
> > definitions there have almost as many differences as similarities.
> >
> > In "reality"? Oh, hell no! I certainly don't know what a
> function is in
> > "reality", but based on the disagreement on this point among
> philosophers of
> > mathematics I'm pretty sure I'm not alone. The one thing I am
> sure of is
> > that it's not the sort of naive Platonism you seem to be
> espousing. If I
> > take a rock and sift it down to constituent quarks I'm pretty
> certain I
> > won't see any functions.
> >
> > How exactly is this helpful to someone who is trying to get some
> work done
> > and complaining that someone else didn't write good doc?
> >
> > --Dave Griffith
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 10:52 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
Hello Ishaaq,
If I have adequately conveyed a point that is provable, has been proven
(by parametricity) and is easily falsifiable, then you'd think I'd hit
less resistance., but alas, it appears not.

You would have had a much easier time if you had stated up-front that you were assuming constructive type theory (or whatever it is that you're actually assuming--you never quite made that clear, though I believe constructive type theory fits), and that you assume that the basic terminology and results of type theory should be a prerequisite for anyone using Scala, and that one should only use Scala in ways consistent with type theory (even though it admits other patterns).

Actually, I don't know if you would have had an easier time, but with that as an assumption about what you meant, yes, what you're saying appears to be proven true--not much room for argument there.

Except I don't think that a signature that is proof of its function _by constructive type theory_ should necessarily be undocumented in Scala.  If you write a library consisting entirely of stuff useful only to people working on constructive type theory, then I absolutely agree that the signature is plenty.

Otherwise, you might want to explain what you're doing in a comment on the method.  At least something like "Obeys all assumptions of constructive type theory."

  --Rex

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

I stated my assumptions at least four times, perhaps more.

I was not assuming anything more than what I stated. Please (at least)
read Theorems for Free, Wadler. Or, if you like take the issue up with
the author of the @free plugin, which, knowingly or not, *proved*
(that's proved) the point way back.

Rex Kerr wrote:
> On Thu, Nov 12, 2009 at 10:52 PM, Tony Morris > wrote:
>
> Hello Ishaaq,
> If I have adequately conveyed a point that is provable, has been
> proven
> (by parametricity) and is easily falsifiable, then you'd think I'd hit
> less resistance., but alas, it appears not.
>
>
> You would have had a much easier time if you had stated up-front that
> you were assuming constructive type theory (or whatever it is that
> you're actually assuming--you never quite made that clear, though I
> believe constructive type theory fits), and that you assume that the
> basic terminology and results of type theory should be a prerequisite
> for anyone using Scala, and that one should only use Scala in ways
> consistent with type theory (even though it admits other patterns).
>
> Actually, I don't know if you would have had an easier time, but with
> that as an assumption about what you meant, yes, what you're saying
> appears to be proven true--not much room for argument there.
>
> Except I don't think that a signature that is proof of its function
> _by constructive type theory_ should necessarily be undocumented in
> Scala. If you write a library consisting entirely of stuff useful
> only to people working on constructive type theory, then I absolutely
> agree that the signature is plenty.
>
> Otherwise, you might want to explain what you're doing in a comment on
> the method. At least something like "Obeys all assumptions of
> constructive type theory."
>
> --Rex
>

bmaso
Joined: 2009-10-04,
User offline. Last seen 2 years 40 weeks ago.
Re: Scaladoc that is actually useful?
I think you meant two different inhabitants that are not reducible to each other, don't you? I mean, the following are equivalent, but different "functions" (your meaning) of the signature "def func[A, B, C](f1: A => B, f2: B => C): A => C"

// keeping it simple
return f2(f1(a));

// bwahahaha
val x = true;
return if(x) { f2(f1(a)) } else { null }

or some other such nonsense reducible to the simple implementation a by sequence of refactorings.

Best regards,
Brian Maso
(949) 395-8551
brian [at] blumenfeld-maso [dot] com
twitter: @bmaso
skype: brian.maso
LinkedIn: http://www.linkedin.com/in/brianmaso

On Thu, Nov 12, 2009 at 7:22 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
So er, back to reality.

Can you provide two inhabitants for:
forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

(Hint: the answer begins with 'n' and ends with 'o').

Dave Griffith wrote:
>
>
> Tony Morris-4 wrote:
>
>> Do you know what function means?
>>
>>
>
> In type theory?  In intuitionistic (a.k.a constructive) type theory? In
> recursive function theory?  In Haskell? In Scala? In C?
>
> Yes, I know what 'function' means, in all of the above.  Even though the
> definitions there have almost as many differences as similarities.
>
> In "reality"?  Oh, hell no!  I certainly don't know what a function is in
> "reality", but based on the disagreement on this point among philosophers of
> mathematics I'm pretty sure I'm not alone.  The one thing I am sure of is
> that it's not the sort of naive Platonism you seem to be espousing.  If I
> take a rock and sift it down to constituent quarks I'm pretty certain I
> won't see any functions.
>
> How exactly is this helpful to someone who is trying to get some work done
> and complaining that someone else didn't write good doc?
>
> --Dave Griffith
>
>

--
Tony Morris
http://tmorris.net/



Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:
> On Thu, Nov 12, 2009 at 7:25 PM, Randall R Schulz wrote:
> > Functions are self-contained and pure. They know not of the world,
> > other than that portion of the world of mathematics that defines
> > them.
>
> ...
>
> It seems highly impractical, however, from a code duplication
> standpoint to never allow a generic function to understand something
> about the types that are thrown at it.

Then the signature exhibits those type constraints.

> So, yes, nice elegance, yay,
> but if I am going to program something, I don't want to have to write
> my composition function over again _in its entirety_ for Int, Float,
> Double, Long, whatever, just so that I keep the type signature
> conforming to the "functions only import the mathematics of their
> arguments" rule.

There's no need. Scala accommodates a single source
for our now classic function composition:

scala> def compose[A, B, C](f: A => B, g: B => C): A => C = { x: A => g(f(x)) }
compose: [A,B,C]((A) => B,(B) => C)(A) => C

scala> def i2f(x: Int): Float = x.toFloat
i2f: (Int)Float

scala> val i2fF = i2f _
i2fF: (Int) => Float =

scala> def f2s(x: Float): String = x.toString
f2s: (Float)String

scala> val f2sF = f2s _
f2sF: (Float) => String =

scala> val i2sF = compose(i2f, f2s)
i2sF: (Int) => String =

scala> i2sF(2)
res0: String = 2.0

> > Programmers have repeatedly been guilty of butchering established
> > concepts and terminology. Calling something a function that does
> > not conform to the definition of function universally agreed upon
> > by mathematicians is inexcusable.
>
> This is absolutely not the definition of function "universally agreed
> upon by mathematicians".
>
> For example,
>
> f(x) : R -> R = {
> x == 0 : 0
> x in Z : 1/x
> else: x
> }
>
> is a perfectly well-defined function on the reals, and it knows all
> about integers which is disallowed by the "pure" function definition
> above.

Where does that function use information outside its definition to alter
what it computes?

> ...
>
> --Rex

Randall Schulz

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

No, null represents a logical absurdity (non-termination). I think you
mean the body of the function may look syntactically different. This may
well be.

Brian Maso wrote:
> I think you meant two different inhabitants that are not reducible to
> each other, don't you? I mean, the following are equivalent, but
> different "functions" (your meaning) of the signature "def func[A, B,
> C](f1: A => B, f2: B => C): A => C"
>
> // keeping it simple
> return f2(f1(a));
>
> // bwahahaha
> val x = true;
> return if(x) { f2(f1(a)) } else { null }
>
> or some other such nonsense reducible to the simple implementation a
> by sequence of refactorings.
>
> Best regards,
> Brian Maso
> (949) 395-8551
> brian [at] blumenfeld-maso [dot] com
> twitter: @bmaso
> skype: brian.maso
> LinkedIn: http://www.linkedin.com/in/brianmaso
>
> On Thu, Nov 12, 2009 at 7:22 PM, Tony Morris > wrote:
>
> So er, back to reality.
>
> Can you provide two inhabitants for:
> forall A B C. (A => B) => (B => C) => A => C
>
> Assume termination and no lies.
>
> (Hint: the answer begins with 'n' and ends with 'o').
>
> Dave Griffith wrote:
> >
> >
> > Tony Morris-4 wrote:
> >
> >> Do you know what function means?
> >>
> >>
> >
> > In type theory? In intuitionistic (a.k.a constructive) type
> theory? In
> > recursive function theory? In Haskell? In Scala? In C?
> >
> > Yes, I know what 'function' means, in all of the above. Even
> though the
> > definitions there have almost as many differences as similarities.
> >
> > In "reality"? Oh, hell no! I certainly don't know what a
> function is in
> > "reality", but based on the disagreement on this point among
> philosophers of
> > mathematics I'm pretty sure I'm not alone. The one thing I am
> sure of is
> > that it's not the sort of naive Platonism you seem to be
> espousing. If I
> > take a rock and sift it down to constituent quarks I'm pretty
> certain I
> > won't see any functions.
> >
> > How exactly is this helpful to someone who is trying to get some
> work done
> > and complaining that someone else didn't write good doc?
> >
> > --Dave Griffith
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

Cay Horstmann
Joined: 2009-09-04,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

Earlier today I agreed with the original poster that there is a
problem with Scaladoc, in that it makes seemingly simple tasks
excessively complex for the programmer who has to get work done. That
discussion went off on some odd tangent about type systems that I will
ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer
in 2.8. The scaladoc sends me to

ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
SeqLike
PartialFunction
Function1
iterableLike
GenericTraversableTemplate
TraversableLike
AnyRef
Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
But then the Scaladoc could have a friendlier way of helping the new
user, such as inline expanding the docs for the traits, or at least,
copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother
knows more type theory than your mother".

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:
> On Thu, Nov 12, 2009 at 11:21 PM, Randall R Schulz wrote:
>
> > > ... I don't want to have to
> > > write my composition function over again _in its entirety_ for
> > > Int, Float, Double, Long, whatever, just so that I keep the type
> > > signature conforming to the "functions only import the
> > > mathematics of their arguments" rule.
> >
> > There's no need. Scala accommodates a single source
> > for our now classic function composition:
>
> That's nice, except my example inverted the sign of numeric inputs by
> matching on the type of the return value of f. Your example doesn't
> do that. What if I want to do that without lots of code duplication?

You're moving the target. I addressed your statement above (copied
here):

> > > ... I don't want to have to
> > > write my composition function over again _in its entirety_ for
> > > Int, Float, Double, Long, whatever

A Scala implementation of your f(x: R): R would compose using the
compose function I showed, assuming a representation of R that meets
whatever criteria you have (obviously floating-point only approximates
the reals).

> ...
> >
> > Where does that function use information outside its definition to
> > alter what it computes?
>
> The reals need not know anything about the integers. ...
>
> Another thing a mathematical function could do ..

I don't know how you read my words, but all these things are functions
that do not use external state to condition what they compute. They are
self-contained, pure functions.

> --Rex

Randall Schulz

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 11:21 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
> So, yes, nice elegance, yay,
> but if I am going to program something, I don't want to have to write
> my composition function over again _in its entirety_ for Int, Float,
> Double, Long, whatever, just so that I keep the type signature
> conforming to the "functions only import the mathematics of their
> arguments" rule.

There's no need. Scala accommodates a single source
for our now classic function composition:

That's nice, except my example inverted the sign of numeric inputs by matching on the type of the return value of f.  Your example doesn't do that.  What if I want to do that without lots of code duplication?
 
> > Programmers have repeatedly been guilty of butchering established
> > concepts and terminology. Calling something a function that does
> > not conform to the definition of function universally agreed upon
> > by mathematicians is inexcusable.
>
> This is absolutely not the definition of function "universally agreed
> upon by mathematicians".
>
> For example,
>
> f(x) : R -> R = {
>   x == 0 : 0
>   x in Z : 1/x
>   else: x
> }
>
> is a perfectly well-defined function on the reals, and it knows all
> about integers which is disallowed by the "pure" function definition
> above.

Where does that function use information outside its definition to alter
what it computes?

The reals need not know anything about the integers.  Thus "x in Z" is an impure operation.  At least, if you pass functions as arguments and you don't get to know about the reals, I don't see why passing reals lets you know about the integers.  (If you don't like that example, I could define the function to test whether cos(i x) is in the upper half of the complex number plane, and even if you construct the reals via the natural number -> rational -> real route, we don't have complex numbers yet, so that would be "out of bounds".)

Another thing a mathematical function could do was notice that if B==C it could return only the output f, or g(f), or g(g(f)) or any other number of compositions since they'd all give a function that mapped as promised.  This is apparently forbidden in constructive type theory.

  --Rex

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

You're moving the target. I addressed your statement above (copied
here):

> > > ... I don't want to have to
> > > write my composition function over again _in its entirety_ for
> > > Int, Float, Double, Long, whatever

No, I'm not moving the target; you're losing the context.  I had a counterexample that went something like

def foo[A,B,C](f: A => B, g: B => C): A => C = {
  (a:A) => {
    val b = f(a)
    g(
      b match {
        case x:Int => -x
        case x:Long => -x
        case x:Float => -x
        case x:Double => -x
        case y => y
      }
    )
  }
}

which absolutely obeys the types _viewed as sets_.  I have constructed a function that, for each input in the set
  (A=>B) x (B=>C)
produces an element in the set
  (A=>C)
which is what is required of a mathematical function.

It is apparently a no-no in type theory.  I can see why as a practical matter: it's got all this ugly fiddling in the middle of it that really won't make proving anything easy.  Is this okay or not?  If not, why not?  What's the difference between asking whether x is in the set of Int and whether x is in the set of natural numbers as in my mathematical examples?

The point is, however, that this sort of inner-fiddling is often quite handy--if a bit dangerous if you don't document your methods and/or give them misleading names--because it avoids most code duplication.

  --Rex

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Cay Horstmann wrote:
> Earlier today I agreed with the original poster that there is a
> problem with Scaladoc, in that it makes seemingly simple tasks
> excessively complex for the programmer who has to get work done. ...
>
> suppose I want to use an ArrayBuffer in 2.8. The scaladoc sends me to
>
> ResizableArray
> Builder
> ...
> AnyRef
> Any
>
> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
> But then the Scaladoc could have a friendlier way of helping the new
> user, such as inline expanding the docs for the traits, or at least,
> copying out the summary method statements.

The Scaladoc HTML is an API reference, not a tutorial. Answers to "how
do I accomplish X" questions don't really belong there, I don't think.

> This really needs some fresh thinking without detours into "my mother
> knows more type theory than your mother".

A comprehensive tutorial introduction to its collection classes, e.g.,
is surely called for. I'm not sure to what extent that qualifies as
fresh thinking, though.

Scala is underdocumented, to be sure. Scarcely any open-source or
academic project at a comparable stage of evolution is.

Randall Schulz

runaro
Joined: 2009-11-13,
User offline. Last seen 32 weeks 2 days ago.
Re: Scaladoc that is actually useful?

> def foo[A,B,C](f: A => B, g: B => C): A => C = {
> (a:A) => {
> val b = f(a)
> g(
> b match {
> case x:Int => -x
> case x:Long => -x
> case x:Float => -x
> case x:Double => -x
> case y => y
> }
> )
> }
> }
>

That has the wrong type. Hint: Any is not C.

runaro
Joined: 2009-11-13,
User offline. Last seen 32 weeks 2 days ago.
Re: Scaladoc that is actually useful?

> That has the wrong type. Hint: Any is not C.
>

Oh, and Scala even gives you a type error:

error: type mismatch;
found : Int
required: B
case x:Int => -x

Good on ya, Scala.

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

I addressed that issue earlier. It's called a type case (see
Data.Typeable). It is indeed a lie (forall A B. A -> B) i.e. the cast
operation.

It is safe to conclude that the proven fact is still indeed a proven
fact and you all have nothing to worry about.

Randall R Schulz wrote:
> On Thursday November 12 2009, Rex Kerr wrote:
>
>> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:
>>
>>> You're moving the target. I addressed your statement above (copied
>>>
>>> here):
>>>
>>>>>> ... I don't want to have to
>>>>>> write my composition function over again _in its entirety_
>>>>>> for Int, Float, Double, Long, whatever
>>>>>>
>> No, I'm not moving the target; you're losing the context.
>>
>
> No, I addressed your point above. What you say below
> is something separate.
>
>
>
>> I had a counterexample that went something like
>>
>> def foo[A,B,C](f: A => B, g: B => C): A => C = {
>> (a:A) => {
>> val b = f(a)
>> g(
>> b match {
>> case x:Int => -x
>> case x:Long => -x
>> case x:Float => -x
>> case x:Double => -x
>> case y => y
>> }
>> )
>> }
>> }
>>
>
> I don't think that's consistent with the universal quantification over
> the type parameters A, B and C? It seems to me you've really conflated
> 5 different functions, four of them with four particular instantiations
> of the type parameter B and one universal in all three type parameters.
>
> One of those four functions is this:
>
> def foo[A, C](f: A => Int, g: Int => c): A => C = {
> x: A => g(-f(x))
> }
>
> There are four other for Long, Float and Double and the generic one I
> gave. The manipulation of the intermediate value is possible because
> the type has been nailed down.
>
> In Tony's terms, your function (or its signature) is a "lie."
>
>
>
>> ...
>>
>> --Rex
>>
>
>
> Randall Schulz
>
>

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:
> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:
> > You're moving the target. I addressed your statement above (copied
> >
> > here):
> > > > > ... I don't want to have to
> > > > > write my composition function over again _in its entirety_
> > > > > for Int, Float, Double, Long, whatever
>
> No, I'm not moving the target; you're losing the context.

No, I addressed your point above. What you say below
is something separate.

> I had a counterexample that went something like
>
> def foo[A,B,C](f: A => B, g: B => C): A => C = {
> (a:A) => {
> val b = f(a)
> g(
> b match {
> case x:Int => -x
> case x:Long => -x
> case x:Float => -x
> case x:Double => -x
> case y => y
> }
> )
> }
> }

I don't think that's consistent with the universal quantification over
the type parameters A, B and C? It seems to me you've really conflated
5 different functions, four of them with four particular instantiations
of the type parameter B and one universal in all three type parameters.

One of those four functions is this:

def foo[A, C](f: A => Int, g: Int => c): A => C = {
x: A => g(-f(x))
}

There are four other for Long, Float and Double and the generic one I
gave. The manipulation of the intermediate value is possible because
the type has been nailed down.

In Tony's terms, your function (or its signature) is a "lie."

> ...
>
> --Rex

Randall Schulz

Maxime Lévesque
Joined: 2009-08-18,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?

 When I first consulted the 2.8 docs I didn't like it, I thought there was a bug.
I got used to it, and now actually prefer it, the boxes (tables) for "methode inherited from"
actually give a more "zoomed out" overall view of what's
available, it's more dense, more info per square centimeter.
But if there's a way to get the best of both worlds, like a
button that woould toggle between an expanded and compressed view
it would certainly be ideal.

  ... I admit to everyone here : My mother is clueless about type theory !!!

  Max


On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:
Earlier today I agreed with the original poster that there is a
problem with Scaladoc, in that it makes seemingly simple tasks
excessively complex for the programmer who has to get work done. That
discussion went off on some odd tangent about type systems that I will
ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer
in 2.8. The scaladoc sends me to

ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
SeqLike
PartialFunction
Function1
iterableLike
GenericTraversableTemplate
TraversableLike
AnyRef
Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
But then the Scaladoc could have a friendlier way of helping the new
user, such as inline expanding the docs for the traits, or at least,
copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother
knows more type theory than your mother".

Ricky Clarkson
Joined: 2008-12-19,
User offline. Last seen 3 years 2 weeks ago.
Re: Scaladoc that is actually useful?

"So I submit that whatever it is that Tony defined is not actually
just a function but is something more strict (perhaps a "pure
function", a subset of the set of all valid functions from the
described input set to the described output set)."

I'm not sure why you would choose to use a non-mathematical definition
of function. The definitions in programming languages don't seem to
be a good base to go from:

C and Common Lisp call every procedure a function.
Pascal calls every procedure with a return value a function.

I'd call Scala's defs 'defs', or 'methods', and refrain from having a
function (instance of Function1 and friends) that is not referentially
transparent, as it's bloody confusing!

I agree with Tony that we should strive to make our types
self-documenting, but add that where they are not, *that* needs
documenting well.

As to the utility of scaladoc, it is awful so I tend to look at the
source instead. At least the source is more amusing.

2009/11/13 Rex Kerr :
> On Thu, Nov 12, 2009 at 7:25 PM, Randall R Schulz wrote:
>>
>> Functions are self-contained and pure. They know not of the world, other
>> than that portion of the world of mathematics that defines them.
>
> Aha. I think this is the key aspect of the idea of "function" that I was
> missing.
>
> In this case, yes, I agree, if functions that take 1-ary functions as
> arguments may only apply operations that are valid on the set of all 1-ary
> functions (and that operation happens to be composition, and you may not
> inspect the arguments or outputs to see if they themselves happen to be in
> the set of all 1-ary functions so you can't do anything there either), there
> is only one possible thing to do: compose the functions.
>
> I suppose that this type of property has nice consequences for provability
> of correctness of programs under some limited situations.
>
> It seems highly impractical, however, from a code duplication standpoint to
> never allow a generic function to understand something about the types that
> are thrown at it. So, yes, nice elegance, yay, but if I am going to program
> something, I don't want to have to write my composition function over again
> _in its entirety_ for Int, Float, Double, Long, whatever, just so that I
> keep the type signature conforming to the "functions only import the
> mathematics of their arguments" rule.
>
>>
>> Programmers have repeatedly been guilty of butchering established
>> concepts and terminology. Calling something a function that does not
>> conform to the definition of function universally agreed upon by
>> mathematicians is inexcusable.
>
> This is absolutely not the definition of function "universally agreed upon
> by mathematicians".
>
> For example,
>
> f(x) : R -> R = {
> x == 0 : 0
> x in Z : 1/x
> else: x
> }
>
> is a perfectly well-defined function on the reals, and it knows all about
> integers which is disallowed by the "pure" function definition above.
>
> The universal definition of function is, in mathematics, something very much
> like this:
>
> A (single-valued) _function_ from set A to set B is a rule that specifies
> for any element a in A an element b in B; we call this element in B f(a).
>
> It says nothing about how it does this. It says nothing about whether it
> knows about real numbers even though its arguments are perhaps functions.
> It just says it maps anything in the input set to some element of the output
> set.
>
> The mathematical definition does not admit side-effects, as it is simply a
> mapping. But it does not forbid _any_ method of transforming input to
> output.
>
> So I submit that whatever it is that Tony defined is not actually just a
> function but is something more strict (perhaps a "pure function", a subset
> of the set of all valid functions from the described input set to the
> described output set). I agree that a "function" that has side-effects is
> not a function in the mathematical sense, except inasmuch as it takes the
> world as an implicit argument and gives it as an implicit return value.
>
> --Rex
>
>

Joshua.Suereth
Joined: 2008-09-02,
User offline. Last seen 32 weeks 5 days ago.
Re: Scaladoc that is actually useful?
I agree 100%!

I also think when you start placing implicits into the mix, you need new ways of documenting things.  Example usage becomes *very* important, especially when every example would show:  import foo.myawesomedsl._   or   class SomeClass extends MyAwesomeDSLTrait

When I first went to learn a few of these DSL-y libraries via scaladoc, it becomes interesting trying to hold all the classes in your head while you drill around looking for methods and types that do nothing but provide handy operators.

- Josh

On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:
Earlier today I agreed with the original poster that there is a
problem with Scaladoc, in that it makes seemingly simple tasks
excessively complex for the programmer who has to get work done. That
discussion went off on some odd tangent about type systems that I will
ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer
in 2.8. The scaladoc sends me to

ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
SeqLike
PartialFunction
Function1
iterableLike
GenericTraversableTemplate
TraversableLike
AnyRef
Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
But then the Scaladoc could have a friendlier way of helping the new
user, such as inline expanding the docs for the traits, or at least,
copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother
knows more type theory than your mother".

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Scaladoc that is actually useful?
It seems I only reply to you on this thread. :-)   Ok, without dismissing the problems with Scala API docs, which I do think it is an important topic, I think the problem here is not quite what you perceive it to be.   Java has relatively small (poor) interfaces, because the language makes it hard to have rich interfaces. Scala, on the other hand, enables very rich interfaces with a low implementation cost.   So, I ask you to consider this... how would you feel if all the methods for all these traits were simply listed one after the other, with their type signatures and descriptions? I don't know about you, but I'd feel tired just by looking at it, before even trying to read it.   When the class makes such extensive use of traits, however, I make use of previous knowledge. It won't help absolute beginners at first, but, at least, you get to reuse the knowledge you have previously acquired.   For instance, I have a fair knowledge of what I can do with an Iterable, so, knowing this class is IterableLike and TraversableLike already tells me a lot of things, without having to look up anything else. The same goes for PartialFunction and Function1.   And that means that, very much contrary to what you have stated, I *only* have to concentrate on:   ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
This is a huge decrease in the number of methods I have to look up. Furthermore, I know a lot of methods I'm used to are present as well.   The alternative, of course, is not having most of these methods and having to reinvent the wheel each time I need something like them.
On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:
Earlier today I agreed with the original poster that there is a
problem with Scaladoc, in that it makes seemingly simple tasks
excessively complex for the programmer who has to get work done. That
discussion went off on some odd tangent about type systems that I will
ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer
in 2.8. The scaladoc sends me to

ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
SeqLike
PartialFunction
Function1
iterableLike
GenericTraversableTemplate
TraversableLike
AnyRef
Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
But then the Scaladoc could have a friendlier way of helping the new
user, such as inline expanding the docs for the traits, or at least,
copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother
knows more type theory than your mother".



--
Daniel C. Sobral

Veni, vidi, veterni.
ounos
Joined: 2008-12-29,
User offline. Last seen 3 years 44 weeks ago.
Re: Scaladoc that is actually useful?

2009/11/13 Tony Morris :
> Unfortunately you have subverted the types. There is no ability to print
> a universal type. This is an unfortunate part of the Java legacy.

So that was the implicit assumption all along. I hope this helps
ending this rather fruitless discussion.

As I said yesterday too, Tony is not really talking about scala, as
you can see above, about the "unfortunate part of the Java legacy". He
talks about an abstraction that he wishes is equivalent to scala. Only
through those glasses/assumptions some docs seem redundant. Yet, Tony
is somehow against documenting assumptions, which is basically a
wishful thinking that the whole scala community will just adopt the
same set of assumptions as he, so he does not need to mention them.

_In scala_, which is the context of discussion, there is a type
hierarchy rooted at Any. For all A, A<:Any. Now, Any is proven to have
a whole range of methods applicable to it, like like hashCode(), like
toString(). So, for all A, one can safely call toString(). I'm sure
someone might scream "subverting!" or "lying!" or "goosfraba!" again
and again but that is completely irrelevant. Point is: in scala, a
signature, even as generic as the aptly named "boo" signature, has
*infinite* different implementations. Knock knock, this is the real
world hitting the door. Now, we can all pretend instead that the real
world is irrelevant, and we could rather reason only through our neat
abstractions, but as someone said, this is kind of Platonic. But
again, Plato was Plato for all his life, wasn't he?

Dimitris

> There is only *one possible answer*.
>
> Rex Kerr wrote:
>> On Thu, Nov 12, 2009 at 3:55 PM, Tony Morris > > wrote:
>>
>>     e.g. What would you (could you possibly) write for this function?
>>     def boo[A, B, C](f: A => B, g: B => C): A => C
>>
>>
>> That one?  I don't know--it's titled "boo", so it should be a
>> surprise.  Maybe it returns a function that prints out "Boo!" and
>> returns null.  Maybe it returns the BooException and never completes
>> normally.
>>
>> How about this one?
>>
>> def printIntermediate[A,B,C](f: A => B, g: B => C): A => C
>>
>> Same type signature.  Maybe it, I don't know, creates a function that
>> prints out the intermediate result of type B in addition to doing the
>> function composition?
>>
>> How about
>>
>> def nullCatch[A,B,C](f: A => B, g: B => C): A => C
>>
>> Same type signature again.  This might possibly catch if inputs are
>> null and throw null outputs rather than throwing exceptions, in
>> addition to composing the functions.
>>
>> If you don't document your functions, how are people supposed to know
>> whether and what side effects there are, and whether the function is
>> value-added (as in nullCatch) or not (as in the straightforward
>> function-composition boo that I assume you were imagining)?
>>
>>   --Rex
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

ounos
Joined: 2008-12-29,
User offline. Last seen 3 years 44 weeks ago.
Re: Scaladoc that is actually useful?

Note though that DSLy things are not bad just in scaladocs - in
javadocs they are a nightmare too.

For example, here is a basic acknowledgement of the fact, in google
guice javadocs:
http://google-guice.googlecode.com/svn/trunk/javadoc/com/google/inject/B...

"Guice uses an embedded domain-specific language, or EDSL, to help you
create bindings simply and readably. This approach is great for
overall usability, but it does come with a small cost: it is difficult
to learn how to use the Binding EDSL by reading method-level javadocs.
"

I think we do need better ways. The various combinations that small
functions can create to yield interesting behavior is lost by just
looking only one by one, in some order, the function definitions
themselves. A graph notation of an api should be promising, but how
would one create an understandable graph of higher-order functions? A
good answer to the latter would immediately open the prospect of a
very interesting project.

Dimitris

2009/11/13 Josh Suereth :
> I agree 100%!
>
> I also think when you start placing implicits into the mix, you need new
> ways of documenting things.  Example usage becomes *very* important,
> especially when every example would show:  import foo.myawesomedsl._   or
> class SomeClass extends MyAwesomeDSLTrait
>
> When I first went to learn a few of these DSL-y libraries via scaladoc, it
> becomes interesting trying to hold all the classes in your head while you
> drill around looking for methods and types that do nothing but provide handy
> operators.
>
> - Josh
>
> On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann
> wrote:
>>
>> Earlier today I agreed with the original poster that there is a
>> problem with Scaladoc, in that it makes seemingly simple tasks
>> excessively complex for the programmer who has to get work done. That
>> discussion went off on some odd tangent about type systems that I will
>> ignore.
>>
>> Back to the original complaint...suppose I want to use an ArrayBuffer
>> in 2.8. The scaladoc sends me to
>>
>> ResizableArray
>> Builder
>> IndexedSeqLike
>> IndexedSeqLike (again, but this time not mutable)
>> BufferLike
>> Shrinkable
>> Growable
>> SeqLike
>> PartialFunction
>> Function1
>> iterableLike
>> GenericTraversableTemplate
>> TraversableLike
>> AnyRef
>> Any
>>
>> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
>> But then the Scaladoc could have a friendlier way of helping the new
>> user, such as inline expanding the docs for the traits, or at least,
>> copying out the summary method statements.
>>
>> This really needs some fresh thinking without detours into "my mother
>> knows more type theory than your mother".
>
>

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Scaladoc that is actually useful?
It doesn't compile.   There are three ways you can go about it:   1. Compose f and g. 2. Do not return (throw an exception, for instance). 3. Return a function that does not return (null, for example).

On Fri, Nov 13, 2009 at 3:00 AM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:
On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

You're moving the target. I addressed your statement above (copied
here):

> > > ... I don't want to have to
> > > write my composition function over again _in its entirety_ for
> > > Int, Float, Double, Long, whatever

No, I'm not moving the target; you're losing the context.  I had a counterexample that went something like

def foo[A,B,C](f: A => B, g: B => C): A => C = {
  (a:A) => {
    val b = f(a)
    g(
      b match {
        case x:Int => -x
        case x:Long => -x
        case x:Float => -x
        case x:Double => -x
        case y => y
      }
    )
  }
}

which absolutely obeys the types _viewed as sets_.  I have constructed a function that, for each input in the set
  (A=>B) x (B=>C)
produces an element in the set
  (A=>C)
which is what is required of a mathematical function.

It is apparently a no-no in type theory.  I can see why as a practical matter: it's got all this ugly fiddling in the middle of it that really won't make proving anything easy.  Is this okay or not?  If not, why not?  What's the difference between asking whether x is in the set of Int and whether x is in the set of natural numbers as in my mathematical examples?

The point is, however, that this sort of inner-fiddling is often quite handy--if a bit dangerous if you don't document your methods and/or give them misleading names--because it avoids most code duplication.

  --Rex




--
Daniel C. Sobral

Veni, vidi, veterni.
dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Scaladoc that is actually useful?
As a side note, I'd love if ScalaDoc provided a search function. I open up a class, type up a method name on the search field, and it either shows me the method definition (in another trait/class, if needed), or tells me it isn't defined for that class.

On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:
Earlier today I agreed with the original poster that there is a
problem with Scaladoc, in that it makes seemingly simple tasks
excessively complex for the programmer who has to get work done. That
discussion went off on some odd tangent about type systems that I will
ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer
in 2.8. The scaladoc sends me to

ResizableArray
Builder
IndexedSeqLike
IndexedSeqLike (again, but this time not mutable)
BufferLike
Shrinkable
Growable
SeqLike
PartialFunction
Function1
iterableLike
GenericTraversableTemplate
TraversableLike
AnyRef
Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
But then the Scaladoc could have a friendlier way of helping the new
user, such as inline expanding the docs for the traits, or at least,
copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother
knows more type theory than your mother".



--
Daniel C. Sobral

Veni, vidi, veterni.
Chris Marshall
Joined: 2009-06-17,
User offline. Last seen 44 weeks 3 days ago.
RE: Scaladoc that is actually useful?
Note that things like the scaladoc for things like the forall function is *ambiguous*:

  /** Return true iff the given predicate `p` yields true for all elements
   *  of this traversable.
   *
   *  @note May not terminate for infinite-sized collections.
   *  @param   p     the predicate
   */

  1. Does this return true for an empty collection? (I don't think the "average" developer is likely to definitively know the answer to this as it's a subtle point of logic.)
  2. Let's say the predicate returns false at the first element - does the implementation of forall continue executing the predicate against the rest of the collection? It might do - the doc doesn't say. What if you are relying on some side-effect (i.e. your predicate is stateful) and not just purely the function result?

Speaking from the perspective of someone who has been bitten *in the real world* by ambiguous or incomplete documentation (String.substring anyone?), extensive documentation of both what the function does and how it does it (or what it may leave undefined) is critical in the long run, although it's understandable that it is something left to last (it's neither a glamorous or interesting thing to do).

I'll say it again: comprehensive documentation creates wider adoption - it's as simple as that.

I am happy to offer my own time to help document scala - how should I go about it?





Use Hotmail to send and receive mail from your different email accounts. Find out how.
Kevin Wright
Joined: 2009-06-09,
User offline. Last seen 49 weeks 3 days ago.
Re: Scaladoc that is actually useful?

Whilst discussing Scaladoc...
What I'd love is a way too see what methods are in scope via
self-typing, and where they originate.

On Fri, Nov 13, 2009 at 2:04 PM, Daniel Sobral wrote:
> As a side note, I'd love if ScalaDoc provided a search function. I open up a
> class, type up a method name on the search field, and it either shows me the
> method definition (in another trait/class, if needed), or tells me it isn't
> defined for that class.
>
> On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann
> wrote:
>>
>> Earlier today I agreed with the original poster that there is a
>> problem with Scaladoc, in that it makes seemingly simple tasks
>> excessively complex for the programmer who has to get work done. That
>> discussion went off on some odd tangent about type systems that I will
>> ignore.
>>
>> Back to the original complaint...suppose I want to use an ArrayBuffer
>> in 2.8. The scaladoc sends me to
>>
>> ResizableArray
>> Builder
>> IndexedSeqLike
>> IndexedSeqLike (again, but this time not mutable)
>> BufferLike
>> Shrinkable
>> Growable
>> SeqLike
>> PartialFunction
>> Function1
>> iterableLike
>> GenericTraversableTemplate
>> TraversableLike
>> AnyRef
>> Any
>>
>> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.
>> But then the Scaladoc could have a friendlier way of helping the new
>> user, such as inline expanding the docs for the traits, or at least,
>> copying out the summary method statements.
>>
>> This really needs some fresh thinking without detours into "my mother
>> knows more type theory than your mother".
>
>
>
> --
> Daniel C. Sobral
>
> Veni, vidi, veterni.
>

David Copeland
Joined: 2009-06-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?
I just can't believe a simple question on this list turned into a 40-deep discussion about type theory and functional programming.  What newcomer would be put off by that? :)

Dave

---
My Blog: http://www.naildrivin5.com/blog
Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour
Fork me on Github: http://davetron5000.github.com



On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
On Thursday November 12 2009, Rex Kerr wrote:
> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:
> > You're moving the target. I addressed your statement above (copied
> >
> > here):
> > > > > ... I don't want to have to
> > > > > write my composition function over again _in its entirety_
> > > > > for Int, Float, Double, Long, whatever
>
> No, I'm not moving the target; you're losing the context.

No, I addressed your point above. What you say below
is something separate.


> I had a counterexample that went something like
>
> def foo[A,B,C](f: A => B, g: B => C): A => C = {
>   (a:A) => {
>     val b = f(a)
>     g(
>       b match {
>         case x:Int => -x
>         case x:Long => -x
>         case x:Float => -x
>         case x:Double => -x
>         case y => y
>       }
>     )
>   }
> }

I don't think that's consistent with the universal quantification over
the type parameters A, B and C? It seems to me you've really conflated
5 different functions, four of them with four particular instantiations
of the type parameter B and one universal in all three type parameters.

One of those four functions is this:

def foo[A, C](f: A => Int, g: Int => c): A => C = {
 x: A => g(-f(x))
}

There are four other for Long, Float and Double and the generic one I
gave. The manipulation of the intermediate value is possible because
the type has been nailed down.

In Tony's terms, your function (or its signature) is a "lie."


> ...
>
>   --Rex


Randall Schulz

David Copeland
Joined: 2009-06-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Scaladoc that is actually useful?
I second this.  Or p(x) => x + 1 it.

I think to assist in this we need:

 - the concept of a doclet (this solves the "show all methods vs. traits" debate, as well as many, many others)
 - an easy to follow means of submitting patches to the docs

I know there was talk of moving the codebase to github.  Is that going to happen?  That would make submitting changes and managing them very easy.


Dave

---
My Blog: http://www.naildrivin5.com/blog
Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour
Fork me on Github: http://davetron5000.github.com



On Fri, Nov 13, 2009 at 9:19 AM, christopher marshall <oxbow_lakes [at] hotmail [dot] com> wrote:
Note that things like the scaladoc for things like the forall function is *ambiguous*:

  /** Return true iff the given predicate `p` yields true for all elements
   *  of this traversable.
   *
   *  @note May not terminate for infinite-sized collections.
   *  @param   p     the predicate
   */

  1. Does this return true for an empty collection? (I don't think the "average" developer is likely to definitively know the answer to this as it's a subtle point of logic.)
  2. Let's say the predicate returns false at the first element - does the implementation of forall continue executing the predicate against the rest of the collection? It might do - the doc doesn't say. What if you are relying on some side-effect (i.e. your predicate is stateful) and not just purely the function result?

Speaking from the perspective of someone who has been bitten *in the real world* by ambiguous or incomplete documentation (String.substring anyone?), extensive documentation of both what the function does and how it does it (or what it may leave undefined) is critical in the long run, although it's understandable that it is something left to last (it's neither a glamorous or interesting thing to do).

I'll say it again: comprehensive documentation creates wider adoption - it's as simple as that.

I am happy to offer my own time to help document scala - how should I go about it?





Use Hotmail to send and receive mail from your different email accounts. Find out how.

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
What you say below is something separate.

> I had a counterexample that went something like
>
> def foo[A,B,C](f: A => B, g: B => C): A => C = {
>   (a:A) => {
>     val b = f(a)
>     g(
>       b match {
>         case x:Int => -x
>         case x:Long => -x
>         case x:Float => -x
>         case x:Double => -x
>         case y => y
>       }
>     )
>   }
> }

I don't think that's consistent with the universal quantification over
the type parameters A, B and C? It seems to me you've really conflated
5 different functions, four of them with four particular instantiations
of the type parameter B and one universal in all three type parameters.

Good grief.  This is *exactly the same* as the test whether a real is an integer except that in some cases the test may always return false depending upon the type of B.  Who cares if a case may always be false?  I have something that maps--if I use proper syntax anyway--from the set of pairs of functions where the domain of one falls within the range of another and gives a function that that maps between the other domain and range.

Granted, Scala doesn't like this, but surely you can stick in a set of if (x.isInstanceOf[Int]) g((-x.asInstanceOf[Int]).asInstanceOf[B]) cases instead to keep the typer happy.  It's *still* a function in the mathematical sense.  Or you can add all 2^32 equality comparisons between x and the values of integers.  It's still a function in the mathematical sense.
 
One of those four functions is this:

def foo[A, C](f: A => Int, g: Int => c): A => C = {
 x: A => g(-f(x))
}

There are four other for Long, Float and Double and the generic one I
gave. The manipulation of the intermediate value is possible because
the type has been nailed down.

In Tony's terms, your function (or its signature) is a "lie."

It's not a lie if it takes the functions it takes and spits out the function it requests, for all A, B, and C.  If it's clever enough to correctly produce a function from A to C given every input, it's a valid function even if it might not be a valid function_as_defined_by_type_theory.

  --Rex

P.S. forall A B. (A -> (A | B)) is not a lie, which is what casting with both "isInstanceOf" and "asInstanceOf" does when it provides a default case.  (Not sure if type theory uses | for "or", or uses v like mathematical logic, or uses something else.)

P.P.S. Ricky--you'd use a non-mathematical definition of function in type theory because you might dislike the sorts of crazy maps between input and output that are valid in a generic (mathematical) function.  By constructing things such that those crazy maps cannot be created (which is what constructive type theory does, as far as I can tell), you get nice theorems about proofs and type-checking being equivalent.
dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Scaladoc that is actually useful?
Scala recommends not using isInstanceOf/asInstanceOf, because you may accidentally lie about types when you use them.   Which proves the point.

On Fri, Nov 13, 2009 at 12:17 PM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:
On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:
What you say below is something separate.

> I had a counterexample that went something like
>
> def foo[A,B,C](f: A => B, g: B => C): A => C = {
>   (a:A) => {
>     val b = f(a)
>     g(
>       b match {
>         case x:Int => -x
>         case x:Long => -x
>         case x:Float => -x
>         case x:Double => -x
>         case y => y
>       }
>     )
>   }
> }

I don't think that's consistent with the universal quantification over
the type parameters A, B and C? It seems to me you've really conflated
5 different functions, four of them with four particular instantiations
of the type parameter B and one universal in all three type parameters.

Good grief.  This is *exactly the same* as the test whether a real is an integer except that in some cases the test may always return false depending upon the type of B.  Who cares if a case may always be false?  I have something that maps--if I use proper syntax anyway--from the set of pairs of functions where the domain of one falls within the range of another and gives a function that that maps between the other domain and range.

Granted, Scala doesn't like this, but surely you can stick in a set of if (x.isInstanceOf[Int]) g((-x.asInstanceOf[Int]).asInstanceOf[B]) cases instead to keep the typer happy.  It's *still* a function in the mathematical sense.  Or you can add all 2^32 equality comparisons between x and the values of integers.  It's still a function in the mathematical sense.
 
One of those four functions is this:

def foo[A, C](f: A => Int, g: Int => c): A => C = {
 x: A => g(-f(x))
}

There are four other for Long, Float and Double and the generic one I
gave. The manipulation of the intermediate value is possible because
the type has been nailed down.

In Tony's terms, your function (or its signature) is a "lie."

It's not a lie if it takes the functions it takes and spits out the function it requests, for all A, B, and C.  If it's clever enough to correctly produce a function from A to C given every input, it's a valid function even if it might not be a valid function_as_defined_by_type_theory.

  --Rex

P.S. forall A B. (A -> (A | B)) is not a lie, which is what casting with both "isInstanceOf" and "asInstanceOf" does when it provides a default case.  (Not sure if type theory uses | for "or", or uses v like mathematical logic, or uses something else.)

P.P.S. Ricky--you'd use a non-mathematical definition of function in type theory because you might dislike the sorts of crazy maps between input and output that are valid in a generic (mathematical) function.  By constructing things such that those crazy maps cannot be created (which is what constructive type theory does, as far as I can tell), you get nice theorems about proofs and type-checking being equivalent.



--
Daniel C. Sobral

Veni, vidi, veterni.
Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Friday November 13 2009, christopher marshall wrote:
> Note that things like the scaladoc for things like the forall
> function is *ambiguous*:
>
> /** Return true iff the given predicate `p` yields true for all
> elements * of this traversable.
> *
> * @note May not terminate for infinite-sized collections.
> * @param p the predicate
> */
>
> Does this return true for an empty collection? (I don't think the
> "average" developer is likely to definitively know the answer to this
> as it's a subtle point of logic.)

It can be rephrased to remove the ambiguity:

"Forall returns false if at least one application of the predicate
returns false."

"Exists returns true if at least one application of the predicate
returns true."

> ...
>
> Speaking from the perspective of someone who has been bitten *in the
> real world* by ambiguous or incomplete documentation

Getting bitten in virtual worlds wouldn't really count, anyway.

And we've all had this experience.

> ...

Randall Schulz

Chris Marshall
Joined: 2009-06-17,
User offline. Last seen 44 weeks 3 days ago.
RE: Scaladoc that is actually useful?
> It can be rephrased to remove the ambiguity:
>
> "Forall returns false if at least one application of the predicate
> returns false."

This is still ambiguous as you've used if instead of iff (which, again, the "average" developer may not be familiar with)! And you still haven't told me whether the implementation will continue to evaluate the predicate after the result of the function is effectively decided (although the original doc about infinite collections gives a hint as to whether this is the case).



Use Hotmail to send and receive mail from your different email accounts. Find out how.
Johannes Rudolph
Joined: 2008-12-17,
User offline. Last seen 29 weeks 19 hours ago.
Re: Scaladoc that is actually useful?

On Fri, Nov 13, 2009 at 3:04 PM, Daniel Sobral wrote:
> As a side note, I'd love if ScalaDoc provided a search function. I open up a
> class, type up a method name on the search field, and it either shows me the
> method definition (in another trait/class, if needed), or tells me it isn't
> defined for that class.

Very helpful: http://www.teria.com/~koseki/tools/gm/javadoc_isearch/index.html

Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Scaladoc that is actually useful?

On Friday November 13 2009, christopher marshall wrote:
> > It can be rephrased to remove the ambiguity:
> >
> > "Forall returns false if at least one application of the predicate
> > returns false."
>
> This is still ambiguous as you've used if instead of iff (which,
> again, the "average" developer may not be familiar with)! And you
> still haven't told me whether the implementation will continue to
> evaluate the predicate after the result of the function is
> effectively decided (although the original doc about infinite
> collections gives a hint as to whether this is the case).

I didn't intend to rewrite the documentation, just show how that one
ambiguity might be expunged.

Randall Schulz

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Scaladoc that is actually useful?
On Fri, Nov 13, 2009 at 9:33 AM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:
Scala recommends not using isInstanceOf/asInstanceOf, because you may accidentally lie about types when you use them.   Which proves the point.

No, all it proves is that you can misuse the constructs that have been supplied.

If you use them to make a whenInstanceOf construct:

def whenInstanceOf[A,B,C](a:A)(f:B=>C):Option[C] = {
  if (a.isInstanceOf[B]) Some(f(a.asInstanceOf[B]))
  else None
}

then you're perfectly typesafe at least as far as set-inclusion goes, unless "isInstanceOf" can't manage to tell what set an object belongs to.

But you can use this whenInstanceOf construct to do things that break the nice this-must-be-function-composition property of Tony's boo-function.

Anyway, I think I've said enough here.  If learning type theory makes one forget what a mathematical function is, that's a pity, but arguing about various sorts of lack of education is a lot less productive than writing better documentation.  So I figure if I'm not going to do the latter, I should be quiet.

  --Rex

Luc Duponcheel
Joined: 2008-12-19,
User offline. Last seen 34 weeks 3 days ago.
Re: Scaladoc that is actually useful?
All,

Without becoming to philosophical, I'd like to add a few thoughts to this
'academically challenging' (e.g. type theory) versus
'industrially acceptable' (e.g. Java) discusson.

Ignore if not interested.

When learning a new programming language there are to mountains to climb

 - its complexity (I use complex as opposed to simple)
 - its difficulty (I use difficult as oppopsed to easy)

Complexity can be reduced using abstraction
(here I use abstraction the software way: as a synonym of symplicifcation).

We should value abstraction because of this!

In my opinion there is no risk associated with this kind of abstraction:
the simpler it gets, the better.

Difficulty can only be demistified, I'm afraid,
and some brains may never understand something that has a certain difficulty.

In general, there is no relationship between complexity and difficulty,
but, something can be so complex that it may seem to be difficult
(our brains can only cope with a limited amount of complexity).

There is also specific versus generic. All to often similar specific code
fragments and similar specific code templates are written.

Reusability can be increased by using abstraction
(here I use abstraction the mathematics way: as a synonym of generalization).

We should value abstraction (maybe even more) because of this!

But, in my opinion there is a risk associated with this kind of abstraction.
First it may increase complexity (Function[-X, +Y] is more complex than Function),
second, and more important, it may increase difficulty (at least for some brains).

So, yes, abstract (in the sense of generic) code should be well documented.
Of course, type information is a very important documentation of it,
but, in my opinion, providing many examples (also in the API documentation!) of
how to use specific instances of it is way more important in order to demistify it.

Some brains tend to learn by specific examples.
Other brains (including my brain) tend to learn by generalization.

Luc

--
  __~O
 -\ <,
(*)/ (*)

reality goes far beyond imagination

Kevin Wright
Joined: 2009-06-09,
User offline. Last seen 49 weeks 3 days ago.
Re: Scaladoc that is actually useful?

I forget who this should be attributed, but I do love the quote:

"There are very few problems in programming that can't be solved by
adding another level of indirection. Except, perhaps, for too much
indirection..."

On Fri, Nov 13, 2009 at 3:35 PM, Luc Duponcheel
wrote:
> All,
>
> Without becoming to philosophical, I'd like to add a few thoughts to this
> 'academically challenging' (e.g. type theory) versus
> 'industrially acceptable' (e.g. Java) discusson.
>
> Ignore if not interested.
>
> When learning a new programming language there are to mountains to climb
>
>  - its complexity (I use complex as opposed to simple)
>  - its difficulty (I use difficult as oppopsed to easy)
>
> Complexity can be reduced using abstraction
> (here I use abstraction the software way: as a synonym of symplicifcation).
>
> We should value abstraction because of this!
>
> In my opinion there is no risk associated with this kind of abstraction:
> the simpler it gets, the better.
>
> Difficulty can only be demistified, I'm afraid,
> and some brains may never understand something that has a certain
> difficulty.
>
> In general, there is no relationship between complexity and difficulty,
> but, something can be so complex that it may seem to be difficult
> (our brains can only cope with a limited amount of complexity).
>
> There is also specific versus generic. All to often similar specific code
> fragments and similar specific code templates are written.
>
> Reusability can be increased by using abstraction
> (here I use abstraction the mathematics way: as a synonym of
> generalization).
>
> We should value abstraction (maybe even more) because of this!
>
> But, in my opinion there is a risk associated with this kind of abstraction.
> First it may increase complexity (Function[-X, +Y] is more complex than
> Function),
> second, and more important, it may increase difficulty (at least for some
> brains).
>
> So, yes, abstract (in the sense of generic) code should be well documented.
> Of course, type information is a very important documentation of it,
> but, in my opinion, providing many examples (also in the API documentation!)
> of
> how to use specific instances of it is way more important in order to
> demistify it.
>
> Some brains tend to learn by specific examples.
> Other brains (including my brain) tend to learn by generalization.
>
> Luc
>
> --
>   __~O
>  -\ <,
> (*)/ (*)
>
> reality goes far beyond imagination
>
>

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland