Re: Scaladoc that is actually useful?

Actually Tony wrote the scaladoc for scala.Either. You'll find it is
complete and comprehensive. I did this entirely appease people like
Andrew. I am "giving Scala a chance" so to speak (whatever that means).

Ismael Juma wrote:
> On Thu, 2009-11-12 at 18:26 -0300, andrew cooke wrote:
>
>> look, take haskell. go educate people with that. let scala have a
>> chance to be successful.
>>
>
> You realise that Tony doesn't influence what goes into the scaladoc for
> the standard library, right?
>
> As far as I know, Martin and others are not against fleshing out the
> scaladoc, they just haven't had the time and no-one else has done it
> either.
>
> Best,
> Ismael
>
>
>

On Fri, 2009-11-13 at 07:38 +1000, Tony Morris wrote:
> Actually Tony wrote the scaladoc for scala.Either.

Yes, I know that (you also wrote the implementation). I just wanted to
make it clear that your comments in that thread did not represent the
opinion of the SVN gatekeepers before another episode like:

http://james-iry.blogspot.com/2008/07/is-scala-for-academics-and-egomani...

> You'll find it is
> complete and comprehensive. I did this entirely appease people like
> Andrew. I am "giving Scala a chance" so to speak (whatever that means).

:)

Best,
Ismael

Yes I do it regularly. This does not mean it is virtuous.

Nils Kilden-Pedersen wrote:
> On Thu, Nov 12, 2009 at 3:38 PM, Tony Morris > wrote:
>
> Actually Tony wrote the scaladoc for scala.Either. You'll find it is
> complete and comprehensive.
>
>
> So you pandered to ill-education?

On Thu, Nov 12, 2009 at 3:38 PM, Tony Morris <tonymorris@gmail.com> wrote:

Actually Tony wrote the scaladoc for scala.Either. You'll find it is
complete and comprehensive.

So you pandered to ill-education?

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*.

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
>

I deliberately left out what I hoped was obvious.

* Side-effects subvert the types. This is invalid. That it is valid in
Scala, does not make it valid in reality. You are not able to compute on
arguments that are not there.
* Assume termination (or solve the halting problem!)

Dave Griffith wrote:
>
> Tony Morris-4 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
>>
>> Not even tests.
>>
>>
>
> def boo[A, B, C](f: A => B, g: B => C): A => C = {
>
> reformatHardDrive();
>
> emptyBankAccount();
>
> error("gotcha")
> }
>
> Not sure I agree 100% with your QA work there.
>
> --Dave Griffith
>

Quite a lot, but that's beside the point. A side-effecting function
accepts the world and returns a pair containing the world.

Do you know what function means?

Dave Griffith wrote:
> Um, what exactly do you think the correlation is between type theory and
> "reality"? That's a
> whole lotta philosophy you're just glossing over, and that's without
> bringing pragmatics
> into it.
>
>
> Tony Morris-4 wrote:
>
>> That it is valid in Scala, does not make it valid in reality.
>>
>>
>
> --Dave Griffith
>
>

Um, what exactly do you think the correlation is between type theory and
"reality"? That's a
whole lotta philosophy you're just glossing over, and that's without
bringing pragmatics
into it.

Tony Morris-4 wrote:
>
> That it is valid in Scala, does not make it valid in reality.
>

--Dave Griffith

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 <tonymorris@gmail.com> 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,

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 <tonymorris@gmail.com> 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 <tonymorris@gmail.com
> <mailto:tonymorris@gmail.com>> 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/

> 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.

What about those people who didn't do CS in school? And if the school can explain stuff to people, why can't the documentation? Honestly, your opinion is one of the most ridiculous things I've heard in a long while: documentation for stuff like APIs is critical, at least *if you want to end up with users.*

Spring or PicoContainer? Spring won because the documentation was superb. Hibernate? The same. Why don't you put yourself in the position of someone who's working to a tight deadline and is trying to understand something unfamiliar. Documentation should be examples, examples and more examples.

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

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*.
>
>

That's the point, they did do CS in school and they still don't
understand some of the basic tenets of computational theory. I find this
lamentable and I am sympathetic toward them for having been robbed by a
self-proclaimed educational institution. I stand firm in my position for
education on this matter, instead of subjects like "Java" or "Web
Programming" as if that is even a subject! It does a disservice to
students, the definition of the term "subject" and results in the
problems that I am observing right now.

I'm not in the business of appeasing ill-education. Documentation for
stuff like APIs is certainly not critical, nor required to have users.

christopher marshall 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.
>
> What about those people who didn't do CS in school? And if the school
> can explain stuff to people, why can't the documentation? Honestly,
> your opinion is one of the most ridiculous things I've heard in a long
> while: documentation for stuff like APIs is critical, at least *if you
> want to end up with users.*
>
> Spring or PicoContainer? Spring won because the documentation was
> superb. Hibernate? The same. Why don't you put yourself in the
> position of someone who's working to a tight deadline and is trying to
> understand something unfamiliar. Documentation should be examples,
> examples and more examples.
>
> ------------------------------------------------------------------------
> Use Hotmail to send and receive mail from your different email
> accounts. Find out how.

No, this is equivalent to solving the halting problem. I am saying we
should strive for using the types and where we cannot, there is still a
much better solution to English -- unfalsified specifications (see
ScalaCheck).

I'd give you such an example, but I'm butting heads on even a simple
one, so I dare not :)

Naftoli Gugenheim wrote:
> Tony, are you saying that the same can be said for every method in the
> Scala API, that it's self explanatory?
>
> On Thu, Nov 12, 2009 at 6:24 PM, Tony Morris > wrote:
>
> 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.
>
> 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/
>
>
>

Hi Randall,
You cannot return a constant, since you have no forall C. C to begin
with. If it were possible, then the statement that it is once-inhabited
would be false! (but of course, it is true)

Randall R Schulz wrote:
> On Thursday November 12 2009, 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.
>>
>
> Nope. The only thing that you can do with these constraints:
>
> Given:
> a) A function from type A to type B (for any types A and B)
> b) A function from type B to type C (for any types B and C)
>
> Yielding:
> c) A function from type A to type C
>
> When the the thing doing the doing is functional (and hence is
> referentially transparent) is to compose those two functions. That is
> uniquely defined. A function—a proper mathematical function, not some
> arbitrary subroutine—say, an arity-two function—when given two
> particular values must always yield the same resulting value. And
> constraining it to be referentially transparent means that it can
> _only_ use its arguments to produce its output.
>
> Hence, the signature fully constrains the function.
>
> If I'm understanding this correctly, there is conceptually one other
> alternative, which is to return a constant function, but I'm not sure
> how to do that generically (i.e., preserving the A => C of the result).
> The only way to do that is to compose the input functions.
>
>
>
>> ...
>>
>> --Rex
>>
>
>
> Randall Schulz
>
>

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.

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/
>
>
>

On Thursday November 12 2009, 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.

Nope. The only thing that you can do with these constraints:

Given:
a) A function from type A to type B (for any types A and B)
b) A function from type B to type C (for any types B and C)

Yielding:
c) A function from type A to type C

When the the thing doing the doing is functional (and hence is
referentially transparent) is to compose those two functions. That is
uniquely defined. A function—a proper mathematical function, not some
arbitrary subroutine—say, an arity-two function—when given two
particular values must always yield the same resulting value. And
constraining it to be referentially transparent means that it can
_only_ use its arguments to produce its output.

Hence, the signature fully constrains the function.

If I'm understanding this correctly, there is conceptually one other
alternative, which is to return a constant function, but I'm not sure
how to do that generically (i.e., preserving the A => C of the result).
The only way to do that is to compose the input functions.

> ...
>
> --Rex

Randall Schulz

Tony, are you saying that the same can be said for every method in the Scala API, that it's self explanatory?

On Thu, Nov 12, 2009 at 6:24 PM, Tony Morris <tonymorris@gmail.com> wrote:

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.

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 <tonymorris@gmail.com
> <mailto:tonymorris@gmail.com>> 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
>     <tonymorris@gmail.com <mailto:tonymorris@gmail.com>
>     > <mailto:tonymorris@gmail.com <mailto:tonymorris@gmail.com>>> 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/

No, it demonstrates that there exist functions for which there are
multiple inhabitants. You gave an example. It raises the question, how
should these ambiguity be resolved? Don't be so fast to reach for an
English description.

The signature I gave is different to yours in that (I absolutely
guarantee) there is only one inhabitant.

Brian Maso wrote:
> (Forgot to send to the list. Der.)
>
> ---------- Forwarded message ----------
> From: *Brian Maso* >
> Date: Thu, Nov 12, 2009 at 3:51 PM
> Subject: Re: [scala-user] Scaladoc that is actually useful?
> To: Randall R Schulz >
>
>
> The following two methods have the signature (Int => String) =>
> (String => Long) => Long, but return different values. Doesn't this
> case demonstrate you're not correct?
>
> def boo(a: Int => String, b: String => Long): Int => Long = {
> def ret(i: Int): Long = {
> return b(a(i));
> }
> return ret;
> }
>
> def boo2(a: Int => String, b: String => Long): Ing => Long = {
> def ret(i: Int): Long = {
> return b(a(i-1) + a(i+1))
> }
> return ret;
> }
>
> Best regards,
> Brian Maso
> (949) 395-8551
> brian@blumenfeld-maso.com
> twitter: @bmaso
> skype: brian.maso
> LinkedIn: http://www.linkedin.com/in/brianmaso
>
>
> On Thu, Nov 12, 2009 at 3:32 PM, Randall R Schulz > wrote:
>
> On Thursday November 12 2009, 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.
>
> Nope. The only thing that you can do with these constraints:
>
> Given:
> a) A function from type A to type B (for any types A and B)
> b) A function from type B to type C (for any types B and C)
>
> Yielding:
> c) A function from type A to type C
>
> When the the thing doing the doing is functional (and hence is
> referentially transparent) is to compose those two functions. That is
> uniquely defined. A function—a proper mathematical function, not some
> arbitrary subroutine—say, an arity-two function—when given two
> particular values must always yield the same resulting value. And
> constraining it to be referentially transparent means that it can
> _only_ use its arguments to produce its output.
>
> Hence, the signature fully constrains the function.
>
> If I'm understanding this correctly, there is conceptually one other
> alternative, which is to return a constant function, but I'm not sure
> how to do that generically (i.e., preserving the A => C of the
> result).
> The only way to do that is to compose the input functions.
>
>
> > ...
> >
> > --Rex
>
>
> Randall Schulz
>
>
>

(Forgot to send to the list. Der.)

---------- Forwarded message ----------
From: Brian Maso <brian@blumenfeld-maso.com>
Date: Thu, Nov 12, 2009 at 3:51 PM
Subject: Re: [scala-user] Scaladoc that is actually useful?
To: Randall R Schulz <rschulz@sonic.net>


The following two methods have the signature (Int => String) => (String => Long) => Long, but return different values. Doesn't this case demonstrate you're not correct?

def boo(a: Int => String, b: String => Long): Int => Long = {
  def ret(i: Int): Long = {
    return b(a(i));
  }
  return ret;
}

def boo2(a: Int => String, b: String => Long): Ing => Long = {
  def ret(i: Int): Long = {
    return b(a(i-1) + a(i+1))
  }
  return ret;
}

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

On Thu, Nov 12, 2009 at 3:32 PM, Randall R Schulz <rschulz@sonic.net> wrote:

On Thursday November 12 2009, 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.

Nope. The only thing that you can do with these constraints:

Given:
a) A function from type A to type B (for any types A and B)
b) A function from type B to type C (for any types B and C)

Yielding:
c) A function from type A to type C

When the the thing doing the doing is functional (and hence is
referentially transparent) is to compose those two functions. That is
uniquely defined. A function—a proper mathematical function, not some
arbitrary subroutine—say, an arity-two function—when given two
particular values must always yield the same resulting value. And
constraining it to be referentially transparent means that it can
_only_ use its arguments to produce its output.

Hence, the signature fully constrains the function.

If I'm understanding this correctly, there is conceptually one other
alternative, which is to return a constant function, but I'm not sure
how to do that generically (i.e., preserving the A => C of the result).
The only way to do that is to compose the input functions.


> ...
>
>   --Rex


Randall Schulz

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/
>
>
>

On Thursday November 12 2009, Brian Maso wrote:
> From: Brian Maso
> Date: Thu, Nov 12, 2009 at 3:51 PM
> Subject: Re: [scala-user] Scaladoc that is actually useful?
> To: Randall R Schulz
>
> The following two methods have the signature (Int => String) =>
> (String => Long) => Long, but return different values. Doesn't this
> case demonstrate you're not correct?

It does not. The type parameters A, B and C are (implicitly) universally
quantified. They range over _all_ types. So you can't just concoct
something and claim it's consistent with the signature of the function
in question.

> ...
>
> Best regards,
> Brian Maso

Randall Schulz

In any case, Tony, you seeming to be working with the mathematical concept of functions (which I have not studied). I don't think the Scaladoc is geared to students of mathematical theory, but to people who make a living by getting computers to perform various tasks (or do so as a hobby), and who feel that they can do so more productively with Scala, with which they are not completely familiar.

On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz <rschulz@sonic.net> wrote:

On Thursday November 12 2009, Brian Maso wrote:
> From: Brian Maso <brian@blumenfeld-maso.com>
> Date: Thu, Nov 12, 2009 at 3:51 PM
> Subject: Re: [scala-user] Scaladoc that is actually useful?
> To: Randall R Schulz <rschulz@sonic.net>
>
> The following two methods have the signature (Int => String) =>
> (String => Long) => Long, but return different values. Doesn't this
> case demonstrate you're not correct?

It does not. The type parameters A, B and C are (implicitly) universally
quantified. They range over _all_ types. So you can't just concoct
something and claim it's consistent with the signature of the function
in question.


> ...
>
> Best regards,
> Brian Maso


Randall Schulz

On Thursday November 12 2009, 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.

Functions are self-contained and pure. They know not of the world, other
than that portion of the world of mathematics that defines them.

A subroutine / method that accesses values not passed to it as arguments
does not compute a function. A method that produces different values
when called repeatedly with the same arguments does not compute a
function.

Not all methods compute functions. And not all signatures are "singly
occupied," and such signatures clearly demand further characterization.

> 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.

It is true Scala programs can readily transgress functional strictures,
but when you say this:

def func[A, B, C](f: A => B, g: B => C): A => C

you've said enough.

It is perfectly correct that to say more (in natural language) is either
redundant or erroneous. Of course, while redundancy isn't a cardinal
sin, erroneousness is.

So tread carefully. Natural language, including "meaningful names" has
equal power to mislead as to enlighten. Formal language is either
understood or not understood. It cannot lie or mislead through
unintended connotations.

> This point has already been made by Rex but lets try it again :)

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.

> Regards,
> Dimitris

Randall Schulz

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/
>>
>>
>>
>>
>
>

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/
>
>
>

I did. I'm not sure what to do about the fact that you have failed to
see that.

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/
>>
>>
>>
>>
>
>

2009/11/13 Randall R Schulz :
> On Thursday November 12 2009, 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.
>
> Functions are self-contained and pure. They know not of the world, other
> than that portion of the world of mathematics that defines them.
>
> A subroutine / method that accesses values not passed to it as arguments
> does not compute a function. A method that produces different values
> when called repeatedly with the same arguments does not compute a
> function.

Why? The world could contain a different B=>C function, and the method
could be using that one instead of the exlicit B=>C argument of it,
while still being a function.

>
> Not all methods compute functions. And not all signatures are "singly
> occupied," and such signatures clearly demand further characterization.
>
>
>> 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.
>
> It is true Scala programs can readily transgress functional strictures,
> but when you say this:
>
>    def func[A, B, C](f: A => B, g: B => C): A => C
>
> you've said enough.
>
> It is perfectly correct that to say more (in natural language) is either
> redundant or erroneous. Of course, while redundancy isn't a cardinal
> sin, erroneousness is.
>
> So tread carefully. Natural language, including "meaningful names" has
> equal power to mislead as to enlighten. Formal language is either
> understood or not understood. It cannot lie or mislead through
> unintended connotations.
>
>
>> This point has already been made by Rex but lets try it again :)
>
> 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.
>
>
>> Regards,
>> Dimitris
>
>
> Randall Schulz
>

On Thursday November 12 2009, Dimitris Andreou wrote:
> 2009/11/13 Randall R Schulz :
> > ...
> >
> > A subroutine / method that accesses values not passed to it as
> > arguments does not compute a function. A method that produces
> > different values when called repeatedly with the same arguments
> > does not compute a function.
>
> Why? The world could contain a different B=>C function, and the
> method could be using that one instead of the exlicit B=>C argument
> of it, while still being a function.

Why?? Because _that's not a function_.

It's just some uncharacterized computation about which can say little
and prove nothing.

Randall Schulz

False dichotomy.

Naftoli Gugenheim wrote:
> In any case, Tony, you seeming to be working with the mathematical
> concept of functions (which I have not studied). I don't think the
> Scaladoc is geared to students of mathematical theory, but to people
> who make a living by getting computers to perform various tasks (or do
> so as a hobby), and who feel that they can do so more productively
> with Scala, with which they are not completely familiar.
>
>
> On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz > wrote:
>
> On Thursday November 12 2009, Brian Maso wrote:
> > From: Brian Maso >
> > Date: Thu, Nov 12, 2009 at 3:51 PM
> > Subject: Re: [scala-user] Scaladoc that is actually useful?
> > To: Randall R Schulz >
> >
> > The following two methods have the signature (Int => String) =>
> > (String => Long) => Long, but return different values. Doesn't this
> > case demonstrate you're not correct?
>
> It does not. The type parameters A, B and C are (implicitly)
> universally
> quantified. They range over _all_ types. So you can't just concoct
> something and claim it's consistent with the signature of the function
> in question.
>
>
> > ...
> >
> > Best regards,
> > Brian Maso
>
>
> Randall Schulz
>
>

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.

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/
>>
>>
>>
>>
>
>

Does the scala library obey those assumptions?

On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris <tonymorris@gmail.com> wrote:

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 <tonymorris@gmail.com>:
>
>> 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 <tonymorris@gmail.com>:
>>>
>>>
>>>> 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 <tonymorris@gmail.com>:
>>>>>
>>>>>
>>>>>
>>>>>> 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 <tonymorris@gmail.com
>>>>>>> <mailto:tonymorris@gmail.com>> 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
>>>>>>>     <tonymorris@gmail.com <mailto:tonymorris@gmail.com>
>>>>>>>     > <mailto:tonymorris@gmail.com <mailto:tonymorris@gmail.com>>> 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/

For the third time, no. No turing-complete language does. Some other
languages do -- one I have used a lot is Coq. Another is Agda. I
recommend both of these to you.

Does this mean it is not a useful question in the context of the issue
of English as a language for documentation? No it doesn't.

Naftoli Gugenheim wrote:
> Does the scala library obey those assumptions?
>
> On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris > wrote:
>
> 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/
>
>
>

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?*

> Date: Fri, 13 Nov 2009 10:19:27 +1000
> From: tonymorris@gmail.com
> To: jim.andreou@gmail.com
> CC: ichoran@gmail.com; scala-user@listes.epfl.ch
> Subject: Re: [scala-user] Scaladoc that is actually useful?
>
> 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 <tonymorris@gmail.com>:
> >
> >> 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 <tonymorris@gmail.com
> >>> <mailto:tonymorris@gmail.com>> 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
> >>> <tonymorris@gmail.com <mailto:tonymorris@gmail.com>
> >>> > <mailto:tonymorris@gmail.com <mailto:tonymorris@gmail.com>>> 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/
>
>

New! Receive and respond to mail from other email accounts from within Hotmail Find out how.

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/
>
>
>

There is an disjoint dichotomy drawn between "the mathematical concept
of functions" and the desire to "people who make a living by getting
computers to perform various tasks..."

Nothing could be further from the truth.

Naftoli Gugenheim wrote:
> I think that answer amounts to circular logic. :) If I misunderstood
> please expand.
>
> On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris > wrote:
>
> False dichotomy.
>
> Naftoli Gugenheim wrote:
> > In any case, Tony, you seeming to be working with the mathematical
> > concept of functions (which I have not studied). I don't think the
> > Scaladoc is geared to students of mathematical theory, but to people
> > who make a living by getting computers to perform various tasks
> (or do
> > so as a hobby), and who feel that they can do so more productively
> > with Scala, with which they are not completely familiar.
> >
> >
> > On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz
>
> > >> wrote:
> >
> > On Thursday November 12 2009, Brian Maso wrote:
> > > From: Brian Maso
> > >>
> > > Date: Thu, Nov 12, 2009 at 3:51 PM
> > > Subject: Re: [scala-user] Scaladoc that is actually useful?
> > > To: Randall R Schulz >>
> > >
> > > The following two methods have the signature (Int =>
> String) =>
> > > (String => Long) => Long, but return different values.
> Doesn't this
> > > case demonstrate you're not correct?
> >
> > It does not. The type parameters A, B and C are (implicitly)
> > universally
> > quantified. They range over _all_ types. So you can't just
> concoct
> > something and claim it's consistent with the signature of
> the function
> > in question.
> >
> >
> > > ...
> > >
> > > Best regards,
> > > Brian Maso
> >
> >
> > Randall Schulz
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>

"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/
>>
>>
>>
>>
>
>

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/
>
>
>

Actually, I didn't claim that at all.

For the fourth time...

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

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/
>>
>>
>>
>>
>
>

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/
>
>
>

I understood what you were referring to. What I do not see is what they have in common with each other.Mathematically, it may be a false dichotomy, but in reality people do not need to be familiar with function theory to program in Scala.

On Thu, Nov 12, 2009 at 7:44 PM, Tony Morris <tonymorris@gmail.com> wrote:

There is an disjoint dichotomy drawn between "the mathematical concept
of functions" and the desire to "people who make a living by getting
computers to perform various tasks..."

Nothing could be further from the truth.

Naftoli Gugenheim wrote:
> I think that answer amounts to circular logic. :) If I misunderstood
> please expand.
>
> On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris <tonymorris@gmail.com
> <mailto:tonymorris@gmail.com>> wrote:
>
>     False dichotomy.
>
>     Naftoli Gugenheim wrote:
>     > In any case, Tony, you seeming to be working with the mathematical
>     > concept of functions (which I have not studied). I don't think the
>     > Scaladoc is geared to students of mathematical theory, but to people
>     > who make a living by getting computers to perform various tasks
>     (or do
>     > so as a hobby), and who feel that they can do so more productively
>     > with Scala, with which they are not completely familiar.
>     >
>     >
>     > On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz
>     <rschulz@sonic.net <mailto:rschulz@sonic.net>
>     > <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>>> wrote:
>     >
>     >     On Thursday November 12 2009, Brian Maso wrote:
>     >     > From: Brian Maso <brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>
>     >     <mailto:brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>>>
>     >     > Date: Thu, Nov 12, 2009 at 3:51 PM
>     >     > Subject: Re: [scala-user] Scaladoc that is actually useful?
>     >     > To: Randall R Schulz <rschulz@sonic.net
>     <mailto:rschulz@sonic.net> <mailto:rschulz@sonic.net
>     <mailto:rschulz@sonic.net>>>
>     >     >
>     >     > The following two methods have the signature (Int =>
>     String) =>
>     >     > (String => Long) => Long, but return different values.
>     Doesn't this
>     >     > case demonstrate you're not correct?
>     >
>     >     It does not. The type parameters A, B and C are (implicitly)
>     >     universally
>     >     quantified. They range over _all_ types. So you can't just
>     concoct
>     >     something and claim it's consistent with the signature of
>     the function
>     >     in question.
>     >
>     >
>     >     > ...
>     >     >
>     >     > Best regards,
>     >     > Brian Maso
>     >
>     >
>     >     Randall Schulz
>     >
>     >
>
>     --
>     Tony Morris
>     http://tmorris.net/
>
>
>

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

On Thu, Nov 12, 2009 at 7:49 PM, Tony Morris <tonymorris@gmail.com> wrote:

If they are familiar with what I prefer to call "computer programming"
(not mathematical theory), then they are certainly more effective when
using Scala. Heck, they at least save time by not writing comments on
their composition function!

Sadly, you have produced yet another false dichotomy between mathematics
and reality. Again, nothing could be further from the truth.

How about we get back to that ever-elusive reality?

 עיין מהר"ל ורמח"ל 

Naftoli Gugenheim wrote:
> I understood what you were referring to. What I do not see is what
> they have in common with each other.
> Mathematically, it may be a false dichotomy, but in reality people do
> not need to be familiar with function theory to program in Scala.
>
> On Thu, Nov 12, 2009 at 7:44 PM, Tony Morris <tonymorris@gmail.com
> <mailto:tonymorris@gmail.com>> wrote:
>
>     There is an disjoint dichotomy drawn between "the mathematical concept
>     of functions" and the desire to "people who make a living by getting
>     computers to perform various tasks..."
>
>     Nothing could be further from the truth.
>
>     Naftoli Gugenheim wrote:
>     > I think that answer amounts to circular logic. :) If I misunderstood
>     > please expand.
>     >
>     > On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris
>     <tonymorris@gmail.com <mailto:tonymorris@gmail.com>
>     > <mailto:tonymorris@gmail.com <mailto:tonymorris@gmail.com>>> wrote:
>     >
>     >     False dichotomy.
>     >
>     >     Naftoli Gugenheim wrote:
>     >     > In any case, Tony, you seeming to be working with the
>     mathematical
>     >     > concept of functions (which I have not studied). I don't
>     think the
>     >     > Scaladoc is geared to students of mathematical theory, but
>     to people
>     >     > who make a living by getting computers to perform various
>     tasks
>     >     (or do
>     >     > so as a hobby), and who feel that they can do so more
>     productively
>     >     > with Scala, with which they are not completely familiar.
>     >     >
>     >     >
>     >     > On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz
>     >     <rschulz@sonic.net <mailto:rschulz@sonic.net>
>     <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>>
>     >     > <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>
>     <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>>>> wrote:
>     >     >
>     >     >     On Thursday November 12 2009, Brian Maso wrote:
>     >     >     > From: Brian Maso <brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>
>     >     <mailto:brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>>
>     >     >     <mailto:brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>
>     >     <mailto:brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>>>>
>     >     >     > Date: Thu, Nov 12, 2009 at 3:51 PM
>     >     >     > Subject: Re: [scala-user] Scaladoc that is actually
>     useful?
>     >     >     > To: Randall R Schulz <rschulz@sonic.net
>     <mailto:rschulz@sonic.net>
>     >     <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>>
>     <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>
>     >     <mailto:rschulz@sonic.net <mailto:rschulz@sonic.net>>>>
>     >     >     >
>     >     >     > The following two methods have the signature (Int =>
>     >     String) =>
>     >     >     > (String => Long) => Long, but return different values.
>     >     Doesn't this
>     >     >     > case demonstrate you're not correct?
>     >     >
>     >     >     It does not. The type parameters A, B and C are
>     (implicitly)
>     >     >     universally
>     >     >     quantified. They range over _all_ types. So you can't just
>     >     concoct
>     >     >     something and claim it's consistent with the signature of
>     >     the function
>     >     >     in question.
>     >     >
>     >     >
>     >     >     > ...
>     >     >     >
>     >     >     > Best regards,
>     >     >     > Brian Maso
>     >     >
>     >     >
>     >     >     Randall Schulz
>     >     >
>     >     >
>     >
>     >     --
>     >     Tony Morris
>     >     http://tmorris.net/
>     >
>     >
>     >
>
>     --
>     Tony Morris
>     http://tmorris.net/
>
>
>

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

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@gmail.com
> > To: oxbow_lakes@hotmail.com
> > CC: jim.andreou@gmail.com; ichoran@gmail.com; scala-user@listes.epfl.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.

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/
>>
>>
>>
>>
>
>

I think that answer amounts to circular logic. :) If I misunderstood please expand.

On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris <tonymorris@gmail.com> wrote:

False dichotomy.

Naftoli Gugenheim wrote:
> In any case, Tony, you seeming to be working with the mathematical
> concept of functions (which I have not studied). I don't think the
> Scaladoc is geared to students of mathematical theory, but to people
> who make a living by getting computers to perform various tasks (or do
> so as a hobby), and who feel that they can do so more productively
> with Scala, with which they are not completely familiar.
>
>
> On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz <rschulz@sonic.net
> <mailto:rschulz@sonic.net>> wrote:
>
>     On Thursday November 12 2009, Brian Maso wrote:
>     > From: Brian Maso <brian@blumenfeld-maso.com
>     <mailto:brian@blumenfeld-maso.com>>
>     > Date: Thu, Nov 12, 2009 at 3:51 PM
>     > Subject: Re: [scala-user] Scaladoc that is actually useful?
>     > To: Randall R Schulz <rschulz@sonic.net <mailto:rschulz@sonic.net>>
>     >
>     > The following two methods have the signature (Int => String) =>
>     > (String => Long) => Long, but return different values. Doesn't this
>     > case demonstrate you're not correct?
>
>     It does not. The type parameters A, B and C are (implicitly)
>     universally
>     quantified. They range over _all_ types. So you can't just concoct
>     something and claim it's consistent with the signature of the function
>     in question.
>
>
>     > ...
>     >
>     > Best regards,
>     > Brian Maso
>
>
>     Randall Schulz
>
>

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

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@gmail.com
> To: oxbow_lakes@hotmail.com
> CC: jim.andreou@gmail.com; ichoran@gmail.com; scala-user@listes.epfl.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.

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 <tonymorris@gmail.com> 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 <tonymorris@gmail.com>:
>
>> 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 <tonymorris@gmail.com>:
>>>
>>>
>>>> "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 <tonymorris@gmail.com>:
>>>>>
>>>>>
>>>>>
>>>>>> 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 <tonymorris@gmail.com>:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> 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 <tonymorris@gmail.com>:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> 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 <tonymorris@gmail.com>:
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> 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 <tonymorris@gmail.com
>>>>>>>>>>>>> <mailto:tonymorris@gmail.com>> 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
>>>>>>>>>>>>>     <tonymorris@gmail.com <mailto:tonymorris@gmail.com>
>>>>>>>>>>>>>     > <mailto:tonymorris@gmail.com <mailto:tonymorris@gmail.com>>> 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/

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/
>>
>>
>>
>>
>
>