- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers

# Re: Scaladoc that is actually useful?

Thu, 2009-11-12, 18:19

Are you sure they're not listed?

In Scala at least the primary constructor is looked at as "the arguments to the class." So it would be listed with documentation of the class itself.

-------------------------------------

Donald McLean wrote:

(observations based on 2.7.7 - feel free to say that something will be

better in 2.8 but only if it actually is)

I'm new to Scala but have been using Java for more than 10 years now.

One of the stumbling blocks that I am running into learning the

language is that the Scaladoc for many of the library classes is

nearly useless. The mutable LinkedList, for example is almost

impossible for a newbie to use because it is so completely unlike most

Java collections and the constructor is not listed in the Scaladoc.

So why aren't constructors listed in the Scaladoc? (though I haven't

yet progressed to the point where the syntax for the LinkedList class

makes sense yet, even if I have figured out how to use it)

And maybe some actual, even useful, descriptive text? If the answer is

"well, nobody has gotten around to it yet," I can understand that (and

will probably volunteer to help correct the problem, just as soon as I

can understand it myself)

Thu, 2009-11-12, 22:47

#2
Re: Scaladoc that is actually useful?

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

Thu, 2009-11-12, 22:57

#3
Re: Scaladoc that is actually useful?

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?

Thu, 2009-11-12, 23:07

#4
Re: Scaladoc that is actually useful?

On Thu, Nov 12, 2009 at 3:38 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

So you pandered to ill-education?

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

complete and comprehensive.

So you pandered to ill-education?

Thu, 2009-11-12, 23:17

#5
Re: Scaladoc that is actually useful?

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

>

Thu, 2009-11-12, 23:27

#6
Re: Scaladoc that is actually useful?

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

>

Thu, 2009-11-12, 23:47

#7
Re: Scaladoc that is actually useful?

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

>

>

Thu, 2009-11-12, 23:57

#8
Re: Scaladoc that is actually useful?

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

Fri, 2009-11-13, 00:17

#9
Re: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

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 [at] gmail [dot] 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*.

Fri, 2009-11-13, 00:17

#10
Re: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

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 [at] gmail [dot] 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 [at] gmail [dot] com

> <mailto:tonymorris [at] gmail [dot] com>> wrote:

>

> Unfortunately you have subverted the types. There is no ability to

> a universal type. This is an unfortunate part of the Java legacy.

>

> There is only *one possible answer*.

>

>

--

Tony Morris

http://tmorris.net/

Fri, 2009-11-13, 00:27

#11
RE: Scaladoc that is actually useful?

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

>

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

Fri, 2009-11-13, 00:37

#12
Re: Scaladoc that is actually useful?

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

>

>

Fri, 2009-11-13, 00:37

#13
Re: Scaladoc that is actually useful?

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.

Fri, 2009-11-13, 00:37

#14
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 00:37

#15
Re: Scaladoc that is actually useful?

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

>

>

Fri, 2009-11-13, 00:47

#16
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 00:47

#17
Re: Scaladoc that is actually useful?

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

Fri, 2009-11-13, 00:57

#18
Re: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

On Thu, Nov 12, 2009 at 6:24 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] gmail [dot] com

> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>>> wrote:

> >

> > Unfortunately you have subverted the types. There is no

> ability to

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

Fri, 2009-11-13, 00:57

#19
Re: Fwd: Scaladoc that is actually useful?

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 [at] blumenfeld-maso [dot] 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

>

>

>

Fri, 2009-11-13, 01:07

#20
Fwd: Scaladoc that is actually useful?

(Forgot to send to the list. Der.)

---------- Forwarded message ----------

From:

Date: Thu, Nov 12, 2009 at 3:51 PM

Subject: Re: [scala-user] Scaladoc that is actually useful?

To: Randall R Schulz <rschulz [at] sonic [dot] 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 [at] blumenfeld-maso [dot] 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 [at] sonic [dot] net> wrote:

---------- Forwarded message ----------

From:

**Brian Maso**<brian [at] blumenfeld-maso [dot] com>Date: Thu, Nov 12, 2009 at 3:51 PM

Subject: Re: [scala-user] Scaladoc that is actually useful?

To: Randall R Schulz <rschulz [at] sonic [dot] 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 [at] blumenfeld-maso [dot] 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 [at] sonic [dot] 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

Fri, 2009-11-13, 01:07

#21
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:17

#22
Re: Fwd: Scaladoc that is actually useful?

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

Fri, 2009-11-13, 01:27

#23
Re: Fwd: Scaladoc that is actually useful?

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 [at] sonic [dot] net> wrote:

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

On Thursday November 12 2009, Brian Maso wrote:

> From: Brian Maso <brian [at] blumenfeld-maso [dot] com>

> Date: Thu, Nov 12, 2009 at 3:51 PM

> Subject: Re: [scala-user] Scaladoc that is actually useful?

> To: Randall R Schulz <rschulz [at] sonic [dot] 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

Fri, 2009-11-13, 01:27

#24
Re: Scaladoc that is actually useful?

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

Fri, 2009-11-13, 01:37

#25
Re: 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 :

>

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

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 01:37

#26
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:37

#27
Re: Scaladoc that is actually useful?

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/

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 01:37

#28
Re: Scaladoc that is actually useful?

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

>

Fri, 2009-11-13, 01:37

#29
Re: Scaladoc that is actually useful?

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

Fri, 2009-11-13, 01:47

#30
Re: Fwd: Scaladoc that is actually useful?

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

>

>

Fri, 2009-11-13, 01:47

#31
Re: 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.

Fri, 2009-11-13, 01:47

#32
Re: Scaladoc that is actually useful?

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/

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 01:47

#33
Re: Scaladoc that is actually useful?

Does the scala library obey those assumptions?

On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] com

>>>>>>> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

>>>>>>> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>>> wrote:

>>>>>>> >

>>>>>>> > Unfortunately you have subverted the types. There is no

>>>>>>> ability to

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

Fri, 2009-11-13, 01:47

#34
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:57

#35
RE: Scaladoc that is actually useful?

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 [at] gmail [dot] com

> To: jim [dot] andreou [at] gmail [dot] com

> CC: ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] com

> >>> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

> >>> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] 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.

> Date: Fri, 13 Nov 2009 10:19:27 +1000

> From: tonymorris [at] gmail [dot] com

> To: jim [dot] andreou [at] gmail [dot] com

> CC: ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] com

> >>> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

> >>> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>>> wrote:

> >>> >

> >>> > Unfortunately you have subverted the types. There is no

> >>> ability to

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

Fri, 2009-11-13, 01:57

#36
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:57

#37
Re: Fwd: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:57

#38
Re: Scaladoc that is actually useful?

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

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 01:57

#39
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 01:57

#40
Re: Scaladoc that is actually useful?

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/

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 02:07

#41
Re: Scaladoc that is actually useful?

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/

>

>

>

Fri, 2009-11-13, 02:07

#42
Re: Fwd: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

On Thu, Nov 12, 2009 at 7:44 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] gmail [dot] com

> <mailto:tonymorris [at] gmail [dot] 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 [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>

> > <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>>> wrote:

> >

> > On Thursday November 12 2009, Brian Maso wrote:

> > > From: Brian Maso <brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>

> > <mailto:brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>>>

> > > Date: Thu, Nov 12, 2009 at 3:51 PM

> > > Subject: Re: [scala-user] Scaladoc that is actually useful?

> > > To: Randall R Schulz <rschulz [at] sonic [dot] net

> <mailto:rschulz [at] sonic [dot] net> <mailto:rschulz [at] sonic [dot] net

> <mailto:rschulz [at] sonic [dot] 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/

Fri, 2009-11-13, 02:07

#43
Re: Fwd: Scaladoc that is actually useful?

On Thu, Nov 12, 2009 at 7:49 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] gmail [dot] com

> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] 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 [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>

> <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>>

> > > <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>

> <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>>>> wrote:

> > >

> > > On Thursday November 12 2009, Brian Maso wrote:

> > > > From: Brian Maso <brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>

> > <mailto:brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>>

> > > <mailto:brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>

> > <mailto:brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>>>>

> > > > Date: Thu, Nov 12, 2009 at 3:51 PM

> > > > Subject: Re: [scala-user] Scaladoc that is actually

> useful?

> > > > To: Randall R Schulz <rschulz [at] sonic [dot] net

> <mailto:rschulz [at] sonic [dot] net>

> > <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>>

> <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] net>

> > <mailto:rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] 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/

Fri, 2009-11-13, 02:07

#44
Re: Scaladoc that is actually useful?

I didn't say that the type signature was all that you needed. I gave a

specific case. It is a fact that, were it not also lamentable, would

also be somewhat amusing that this is causing a "debate."

If you wish to understand why => means implication and why Either means

disjunction and why Tuple2 means conjunction and ..., then I direct you

to any introduction to the Curry-Howard isomorphism, also known as (wait

for it!), Types as Theorems.

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

Theorems.

I am too exhausted to pursue this matter. I was hoping for a different

outcome. Hopefully the silent audience did some thinking!

christopher marshall wrote:

> How does a function:

>

> def foo(i: Int) : String

>

> Tell me anything about what the function *actually does*, regardless

> of whether, under some given definition of "implies" the statement Int

> => String is "true", given foo. I must be completely missing some

> point here because for the life of me I don't really understand the

> train of thought that says that the type signature of a function is

> all you need to parse to understand what the function does.

>

> > Date: Fri, 13 Nov 2009 10:31:34 +1000

> > From: tonymorris [at] gmail [dot] com

> > To: oxbow_lakes [at] hotmail [dot] com

> > CC: jim [dot] andreou [at] gmail [dot] com; ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch

> > Subject: Re: [scala-user] Scaladoc that is actually useful?

> >

> >

> >

> > christopher marshall wrote:

> > > The fact that you are using => to mean the mathematical/logic

> > > "implies" seems to ignore the fact that in Scala, => means no such

> > > thing. A, B and C are not statements/sentences: in a scala signature,

> > > they are types and the signature tells me nothing about what the

> > > method/function actually does! *Why are we even arguing about this?*

> >

> > Actually, in Scala it means exactly that. Please see the C-H

> Isomorphism.

> >

> > --

> > Tony Morris

> > http://tmorris.net/

> >

> >

>

> ------------------------------------------------------------------------

> Use Hotmail to send and receive mail from your different email

> accounts. Find out how.

Fri, 2009-11-13, 02:07

#45
Re: Scaladoc that is actually useful?

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/

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 02:17

#46
Re: Fwd: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] sonic [dot] net

> <mailto:rschulz [at] sonic [dot] net>> wrote:

>

> On Thursday November 12 2009, Brian Maso wrote:

> > From: Brian Maso <brian [at] blumenfeld-maso [dot] com

> <mailto:brian [at] blumenfeld-maso [dot] com>>

> > Date: Thu, Nov 12, 2009 at 3:51 PM

> > Subject: Re: [scala-user] Scaladoc that is actually useful?

> > To: Randall R Schulz <rschulz [at] sonic [dot] net <mailto:rschulz [at] sonic [dot] 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/

Fri, 2009-11-13, 02:17

#47
RE: Scaladoc that is actually useful?

How does a function:

def foo(i: Int) : String

Tell me anything about what the function *actually does*, regardless of whether, under some given definition of "implies" the statement Int => String is "true", given foo. I must be completely missing some point here because for the life of me I don't really understand the train of thought that says that the type signature of a function is all you need to parse to understand what the function does.

> Date: Fri, 13 Nov 2009 10:31:34 +1000

> From: tonymorris [at] gmail [dot] com

> To: oxbow_lakes [at] hotmail [dot] com

> CC: jim [dot] andreou [at] gmail [dot] com; ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch

> Subject: Re: [scala-user] Scaladoc that is actually useful?

>

>

>

> christopher marshall wrote:

> > The fact that you are using => to mean the mathematical/logic

> > "implies" seems to ignore the fact that in Scala, => means no such

> > thing. A, B and C are not statements/sentences: in a scala signature,

> > they are types and the signature tells me nothing about what the

> > method/function actually does! *Why are we even arguing about this?*

>

> Actually, in Scala it means exactly that. Please see the C-H Isomorphism.

>

> --

> Tony Morris

> http://tmorris.net/

>

>

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

def foo(i: Int) : String

Tell me anything about what the function *actually does*, regardless of whether, under some given definition of "implies" the statement Int => String is "true", given foo. I must be completely missing some point here because for the life of me I don't really understand the train of thought that says that the type signature of a function is all you need to parse to understand what the function does.

> Date: Fri, 13 Nov 2009 10:31:34 +1000

> From: tonymorris [at] gmail [dot] com

> To: oxbow_lakes [at] hotmail [dot] com

> CC: jim [dot] andreou [at] gmail [dot] com; ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch

> Subject: Re: [scala-user] Scaladoc that is actually useful?

>

>

>

> christopher marshall wrote:

> > The fact that you are using => to mean the mathematical/logic

> > "implies" seems to ignore the fact that in Scala, => means no such

> > thing. A, B and C are not statements/sentences: in a scala signature,

> > they are types and the signature tells me nothing about what the

> > method/function actually does! *Why are we even arguing about this?*

>

> Actually, in Scala it means exactly that. Please see the C-H Isomorphism.

>

> --

> Tony Morris

> http://tmorris.net/

>

>

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

Fri, 2009-11-13, 02:17

#48
Re: Scaladoc that is actually useful?

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 [at] gmail [dot] com> wrote:

On Thu, Nov 12, 2009 at 8:04 PM, Tony Morris <tonymorris [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] 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 [at] gmail [dot] com

>>>>>>>>>>>>> <mailto:tonymorris [at] gmail [dot] 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 [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>

>>>>>>>>>>>>> > <mailto:tonymorris [at] gmail [dot] com <mailto:tonymorris [at] gmail [dot] com>>> wrote:

>>>>>>>>>>>>> >

>>>>>>>>>>>>> > Unfortunately you have subverted the types. There is no

>>>>>>>>>>>>> ability to

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

Fri, 2009-11-13, 02:17

#49
Re: Scaladoc that is actually useful?

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/

>>

>>

>>

>>

>

>

Fri, 2009-11-13, 02:27

#50
Re: Fwd: Scaladoc that is actually useful?

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

>

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

> >

> >

> >

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

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

>

>

>