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

# Re: Scaladoc that is actually useful?

Fri, 2009-11-13, 02:27

#52
Re: Scaladoc that is actually useful?

The interesting part is the conclusion, once-inhabited. And the

indisputable conclusion: "it is impossible to write tests or even

documentation for this function without redundancy or error."

We could get to other cases and whether it is safe to make these

assumptions, but look how much effort it took to get this far.

Naftoli Gugenheim wrote:

> Now I'm very confused.

> So methods that don't conform to these assumptions should indeed have

> English scaladocs? Or just ScalaCheck tests? And how would one browse

> them?

>

>

> On Thu, Nov 12, 2009 at 8:04 PM, Tony Morris > wrote:

>

> Please don't be dishonest. This is the *fourth time*.

>

> Let's restate the assumptions:

>

> * Assume termination

> * No subverting the types

>

> Dimitris Andreou wrote:

> > 2009/11/13 Tony Morris >:

> >

> >> Actually, I didn't claim that at all.

> >>

> >

> > Erm... "I assure you, the signature given is once-inhabited" -

> and you

> > kind of insisted that you were talking about scala...

> >

> >

> >> For the fourth time...

> >>

> >> ah bugger it. And no, the halting problem does not contradict

> that at

> >> all (ugh!).

> >>

> >

> > But you are right about that, of course. It doesn't take a halting

> > problem to prove that there are non-terminating implementations

> (which

> > simultaneously conform to the supposedly once-habitated signature

> > though!), one can just create a trivial example.

> >

> > Bye!

> >

> >> Dimitris Andreou wrote:

> >>

> >>> Since *you* claimed that there was only a single implementation of

> >>> that signature, it is *you* that imply that all possible

> >>> implementations are halting. Guess what, that's exactly what the

> >>> halting problem contradicts :)

> >>>

> >>> See you! It was fun :)

> >>> I really like you you know, but sometimes I think you just rant

> >>> unchecked (with no suppress compiler option :) )

> >>>

> >>> Good night all,

> >>> Dimitris

> >>>

> >>> 2009/11/13 Tony Morris >:

> >>>

> >>>

> >>>> "I am not discussing this matter any further until you have

> solved the

> >>>> turing halting problem!"

> >>>>

> >>>> That's fine by me, I'm exhausted :) Seeya!

> >>>>

> >>>> Dimitris Andreou wrote:

> >>>>

> >>>>

> >>>>> Omg, you used...english! Please encode these constrains as a

> scala

> >>>>> signature and I go home. :)

> >>>>>

> >>>>> 2009/11/13 Tony Morris >:

> >>>>>

> >>>>>

> >>>>>

> >>>>>> You seem to have overlooked some important parts. I will

> repeat them for

> >>>>>> a third time:

> >>>>>>

> >>>>>> * No subverting the types

> >>>>>> * Assume termination

> >>>>>>

> >>>>>> *crosses fingers*

> >>>>>>

> >>>>>> Dimitris Andreou wrote:

> >>>>>>

> >>>>>>

> >>>>>>

> >>>>>>> 2009/11/13 Tony Morris >:

> >>>>>>>

> >>>>>>>

> >>>>>>>

> >>>>>>>

> >>>>>>>> I did. I'm not sure what to do about the fact that you

> have failed to

> >>>>>>>> see that.

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>> I hope that was *not* your favourite line as a lecturer :)

> >>>>>>>

> >>>>>>> This is the signature I see you gave:

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

> >>>>>>>

> >>>>>>> It does not constrain "boo" (scala) implementations from

> using the

> >>>>>>> implicit world. So you did not address my request. If you

> gave another

> >>>>>>> signature I missed, please repeat.

> >>>>>>>

> >>>>>>> Dimitris

> >>>>>>>

> >>>>>>>

> >>>>>>>

> >>>>>>>

> >>>>>>>

> >>>>>>>> Dimitris Andreou wrote:

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>> As I said, please give us a scala signature that

> constrains its body

> >>>>>>>>> from not using the world. Otherwise, I would be very

> happy to see how

> >>>>>>>>> exactly you encode the mathematical signature into a

> scala signature

> >>>>>>>>> which also has just one implementation. Thank you.

> >>>>>>>>>

> >>>>>>>>> 2009/11/13 Tony Morris >:

> >>>>>>>>>

> >>>>>>>>>

> >>>>>>>>>

> >>>>>>>>>

> >>>>>>>>>

> >>>>>>>>>> It's entirely possible to construct a de-facto world

> state. The

> >>>>>>>>>> signature definitely does have just one instance. It

> definitely does.

> >>>>>>>>>> There is a proof. The strongest possible claim about

> reality exists.

> >>>>>>>>>> There's not much I can do about the fact that you are

> refuting a proof

> >>>>>>>>>> by simply asserting the contrary. I'd move this to

> scala-debate but it's

> >>>>>>>>>> not even a debate.

> >>>>>>>>>>

> >>>>>>>>>> I talk about *functions* and definitely Scala

> programming. I'm well

> >>>>>>>>>> aware that Scala does not have an effect system. The

> question arises,

> >>>>>>>>>> what shall we do about it? The answer is not English.

> Rex hasn't already

> >>>>>>>>>> made this point -- *I* have already made this point.

> >>>>>>>>>>

> >>>>>>>>>> I will repeat myself:

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

> >>>>>>>>>>

> >>>>>>>>>> No subverting the types, assume termination -->

> once-inhabited!

> >>>>>>>>>>

> >>>>>>>>>> I am exhausted, you win.

> >>>>>>>>>>

> >>>>>>>>>> Dimitris Andreou wrote:

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>> 2009/11/13 Tony Morris >:

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

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

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

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

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

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

> >>>>>>>>>>>> Rex,

> >>>>>>>>>>>> I can read your code just fine. I assure you, the

> signature given is

> >>>>>>>>>>>> once-inhabited. There is even a proof of this fact.

> It's a well

> >>>>>>>>>>>> understood basic fact of computational theory.

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

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

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

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

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

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

> >>>>>>>>>>> The problem is that a signature never captures the

> implicit "world"

> >>>>>>>>>>> argument that all functions have (otherwise, please

> show me your

> >>>>>>>>>>> functions having the "world" argument from which you

> access all of

> >>>>>>>>>>> scala libraries) . So the signature definitely has

> *not* just one

> >>>>>>>>>>> instance, but infinitely many.

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

> >>>>>>>>>>> If you don't assume that a function is able to compute

> other

> >>>>>>>>>>> functions, just because it didn't have them as

> arguments, you talk

> >>>>>>>>>>> about something else but definitely not about scala

> programming. May I

> >>>>>>>>>>> remind that the discussion is about _scala_ docs.

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

> >>>>>>>>>>> This point has already been made by Rex but lets try

> it again :)

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

> >>>>>>>>>>> Regards,

> >>>>>>>>>>> Dimitris

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

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

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

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

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

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

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

> >>>>>>>>>>>> So, the question arises, where are you wrong? The

> theorem: forall A B. A

> >>>>>>>>>>>> -> B is also known as "the cast operator." Under the

> Curry-Howard

> >>>>>>>>>>>> Isomorphism, functions are implication -- that is why

> we denote them

> >>>>>>>>>>>> with -> symbol.

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

> >>>>>>>>>>>> Let's draw the truth table for implication:

> >>>>>>>>>>>> P Q P->Q

> >>>>>>>>>>>> 0 0 1

> >>>>>>>>>>>> 0 1 1

> >>>>>>>>>>>> 1 0 0

> >>>>>>>>>>>> 1 1 1

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

> >>>>>>>>>>>> So we have a premise and a conclusion in one. We see

> immediately that

> >>>>>>>>>>>> this is not tautological. Therefore, forall A B. A ->

> B is not a

> >>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting

> Erik Meijer at a

> >>>>>>>>>>>> conference in front about ~400 typical programmers,

> "It is a LIE!"

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

> >>>>>>>>>>>> Scala's type systems has many "let's escape reality

> and tell lies." One

> >>>>>>>>>>>> of them is side-effects, another is casting. Haskell,

> which also does

> >>>>>>>>>>>> same, calls the former unsafePerformIO and the latter

> unsafeCoerce. The

> >>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these

> functions tell lies."

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

> >>>>>>>>>>>> The question can be phrased in English as "tell the

> truth about this

> >>>>>>>>>>>> signature." This means no lies, no subverting the

> types. No def cast[A,

> >>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you

> use them is the

> >>>>>>>>>>>> extent that you are telling lies (and so we must not

> get *all* our

> >>>>>>>>>>>> documentation from types, but we should strive for it

> as a virtue).

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

> >>>>>>>>>>>> I really hope this helps. This is exhausting.

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

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

> >>>>>>>>>>>> Rex Kerr wrote:

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

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

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

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

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

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

> >>>>>>>>>>>>> Tony,

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

> >>>>>>>>>>>>> I'm not convinced you're paying attention to my

> code, and if you are,

> >>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.

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

> >>>>>>>>>>>>> Please explain exactly where the subversion occurs,

> and please say

> >>>>>>>>>>>>> exactly what the return type should be for the

> Double square

> >>>>>>>>>>>>> function. If the return type for the Double

> function is not Double,

> >>>>>>>>>>>>> please explain what the return type is for the F(n)

> function which

> >>>>>>>>>>>>> computes the n'th Fibonacci number.

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

> >>>>>>>>>>>>> Or you can come up with some alternate scheme that

> will demonstrate

> >>>>>>>>>>>>> that you are actually understanding what I am saying

> and disagreeing

> >>>>>>>>>>>>> on the basis of solid principles.

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

> >>>>>>>>>>>>> (Or, of course, we can just drop it.)

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

> >>>>>>>>>>>>> --Rex

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

> >>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris

>

> >>>>>>>>>>>>> >> wrote:

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

> >>>>>>>>>>>>> You've subverted the types again. forall A B. A

> -> B is not a theorem.

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

> >>>>>>>>>>>>> I assure you, there is only one possible

> solution and I didn't

> >>>>>>>>>>>>> just make

> >>>>>>>>>>>>> it up. I refer back to my lobbying for basic

> type theory in schools. I

> >>>>>>>>>>>>> predict we wouldn't be having this discussion,

> but a more

> >>>>>>>>>>>>> interesting one.

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

> >>>>>>>>>>>>> Rex Kerr wrote:

> >>>>>>>>>>>>> > There are infinitely many possible answers to

> what can happen with

> >>>>>>>>>>>>> > that type signature, given that A and B can be

> any type. What

> >>>>>>>>>>>>> if foo

> >>>>>>>>>>>>> > picks out certain Bs and converts them to

> different B's, while

> >>>>>>>>>>>>> leaving

> >>>>>>>>>>>>> > everything else alone? The type system *only

> says that boo gives a

> >>>>>>>>>>>>> > function that takes A and returns C*. It

> doesn't say anything about

> >>>>>>>>>>>>> > how. There's an obvious path, and lots of

> non-obvious paths that

> >>>>>>>>>>>>> > might have practical utility.

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

> >>>>>>>>>>>>> > For example,

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

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

> >>>>>>>>>>>>> > new (a:A) => (c:C) {

> >>>>>>>>>>>>> > val b = f(a)

> >>>>>>>>>>>>> > g(

> >>>>>>>>>>>>> > b match {

> >>>>>>>>>>>>> > case x:Int : -x

> >>>>>>>>>>>>> > case x:Long : -x

> >>>>>>>>>>>>> > case x:Float : -x

> >>>>>>>>>>>>> > case x:Double: -x

> >>>>>>>>>>>>> > case y: y

> >>>>>>>>>>>>> > }

> >>>>>>>>>>>>> > )

> >>>>>>>>>>>>> > }

> >>>>>>>>>>>>> > }

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

> >>>>>>>>>>>>> > (I didn't run this, so there may be syntax

> errors, but you get

> >>>>>>>>>>>>> the idea.)

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

> >>>>>>>>>>>>> > This is *entirely fine* by the type system.

> It takes exactly

> >>>>>>>>>>>>> what is

> >>>>>>>>>>>>> > promised, has no side effects whatsoever, and

> returns exactly

> >>>>>>>>>>>>> what is

> >>>>>>>>>>>>> > promised.

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

> >>>>>>>>>>>>> > Sure, there are now some subset of inputs that

> may have had

> >>>>>>>>>>>>> one-to-one

> >>>>>>>>>>>>> > mappings that now are not, but that's not the

> type system's job to

> >>>>>>>>>>>>> > handle. (Unless, of course, you think that def

> >>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the

> proper type signature for

> >>>>>>>>>>>>> > the x*x operation; in that case, I'd just

> point out that such a type

> >>>>>>>>>>>>> > system is impractical.)

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

> >>>>>>>>>>>>> > --Rex

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

> >>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris

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

> >>>>>>>>>>>>> > >>> wrote:

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

> >>>>>>>>>>>>> > Unfortunately you have subverted the

> types. There is no

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

> >>>>>>>>>>>>> > print

> >>>>>>>>>>>>> > a universal type. This is an unfortunate

> part of the Java

> >>>>>>>>>>>>> legacy.

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

> >>>>>>>>>>>>> > There is only *one possible answer*.

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

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

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

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

> >>>>>>>>>>>>> Tony Morris

> >>>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

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

> >>>>>>>>>>>> Tony Morris

> >>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

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

> >>>>>>>>>> Tony Morris

> >>>>>>>>>> http://tmorris.net/

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>>>>

> >>>>>>>> --

> >>>>>>>> Tony Morris

> >>>>>>>> http://tmorris.net/

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>>>>

> >>>>>> --

> >>>>>> Tony Morris

> >>>>>> http://tmorris.net/

> >>>>>>

> >>>>>>

> >>>>>>

> >>>>>>

> >>>>>>

> >>>>>>

> >>>> --

> >>>> Tony Morris

> >>>> http://tmorris.net/

> >>>>

> >>>>

> >>>>

> >>>>

> >>>>

> >>>

> >> --

> >> Tony Morris

> >> http://tmorris.net/

> >>

> >>

> >>

> >>

> >

> >

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 02:27

#53
Re: Scaladoc that is actually useful?

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

this exhaustive discussion.

There are other interesting facts to be made from here too! I only gave

a trivial and easy to prove (haha!) case for the purpose of discussing

Scaladoc.

Someone else (nameless for now) found it "interesting" that it was even

a discussion worth having, and felt it most appropriate to simply

conclude (see free theorems):

> @free cmp :: (b -> c) -> (a -> b) -> (a -> c)

> g . k = p . f => f . q = f1 . h => g . cmp k q = cmp p f1 . h

Brian Maso wrote:

> Well, I think we understand how there is only one definition of

> def func[A, B, C](f1: A=>B, f2: B=>C): A=>C

>

> when there are no constraints on A, B, or C, and where no implicit

> values or contextual (imported) values are used in the body of the

> function. That is, for *all* A, B and C (as opposed to for *some* A, B

> and C, which is how I had misread the original). That's actually

> mildly interesting. Not sure how I'm going to use that in the future,

> or the rest of Types as Theories, to build webpages faster... Now

> *that* would be a great college course!

>

> Best regards,

> Brian Maso

> (949) 395-8551

> brian [at] blumenfeld-maso [dot] com

> twitter: @bmaso

> skype: brian.maso

> LinkedIn: http://www.linkedin.com/in/brianmaso

>

>

> On Thu, Nov 12, 2009 at 5:03 PM, Tony Morris > wrote:

>

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

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

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

>

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

> means

> disjunction and why Tuple2 means conjunction and ..., then I

> direct you

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

> (wait

> for it!), Types as Theorems.

>

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

> Theorems.

>

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

> outcome. Hopefully the silent audience did some thinking!

>

> christopher marshall wrote:

> > How does a function:

> >

> > def foo(i: Int) : String

> >

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

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

> statement Int

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

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

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

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

> >

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

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

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

> > > CC: jim [dot] andreou [at] gmail [dot] com ;

> ichoran [at] gmail [dot] com ;

> scala-user [at] listes [dot] epfl [dot] ch

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

> > >

> > >

> > >

> > > christopher marshall wrote:

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

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

> no such

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

> signature,

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

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

> about this?*

> > >

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

> > Isomorphism.

> > >

> > > --

> > > Tony Morris

> > > http://tmorris.net/

> > >

> > >

> >

> >

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

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

> > accounts. Find out how.

>

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 02:27

#54
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:

> Still need some language (e.g. english) to describe these

> assumptions. They are not axioms you know or theorems, they

> are...argh...assumptions. Please document your assumptions! Please

> ask students to document their assumptions :)

That is precisely what they are, axioms.

Randall Schulz

Fri, 2009-11-13, 02:37

#55
Re: Scaladoc that is actually useful?

2009/11/13 Tony Morris :

> Actually, I didn't claim that at all.

Erm... "I assure you, the signature given is once-inhabited" - and you

kind of insisted that you were talking about scala...

>

> For the fourth time...

>

> ah bugger it. And no, the halting problem does not contradict that at

> all (ugh!).

But you are right about that, of course. It doesn't take a halting

problem to prove that there are non-terminating implementations (which

simultaneously conform to the supposedly once-habitated signature

though!), one can just create a trivial example.

Bye!

>

> Dimitris Andreou wrote:

>> Since *you* claimed that there was only a single implementation of

>> that signature, it is *you* that imply that all possible

>> implementations are halting. Guess what, that's exactly what the

>> halting problem contradicts :)

>>

>> See you! It was fun :)

>> I really like you you know, but sometimes I think you just rant

>> unchecked (with no suppress compiler option :) )

>>

>> Good night all,

>> Dimitris

>>

>> 2009/11/13 Tony Morris :

>>

>>> "I am not discussing this matter any further until you have solved the

>>> turing halting problem!"

>>>

>>> That's fine by me, I'm exhausted :) Seeya!

>>>

>>> Dimitris Andreou wrote:

>>>

>>>> Omg, you used...english! Please encode these constrains as a scala

>>>> signature and I go home. :)

>>>>

>>>> 2009/11/13 Tony Morris :

>>>>

>>>>

>>>>> You seem to have overlooked some important parts. I will repeat them for

>>>>> a third time:

>>>>>

>>>>> * No subverting the types

>>>>> * Assume termination

>>>>>

>>>>> *crosses fingers*

>>>>>

>>>>> Dimitris Andreou wrote:

>>>>>

>>>>>

>>>>>> 2009/11/13 Tony Morris :

>>>>>>

>>>>>>

>>>>>>

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

>>>>>>> see that.

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>> I hope that was *not* your favourite line as a lecturer :)

>>>>>>

>>>>>> This is the signature I see you gave:

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

>>>>>>

>>>>>> It does not constrain "boo" (scala) implementations from using the

>>>>>> implicit world. So you did not address my request. If you gave another

>>>>>> signature I missed, please repeat.

>>>>>>

>>>>>> Dimitris

>>>>>>

>>>>>>

>>>>>>

>>>>>>

>>>>>>> Dimitris Andreou wrote:

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>> As I said, please give us a scala signature that constrains its body

>>>>>>>> from not using the world. Otherwise, I would be very happy to see how

>>>>>>>> exactly you encode the mathematical signature into a scala signature

>>>>>>>> which also has just one implementation. Thank you.

>>>>>>>>

>>>>>>>> 2009/11/13 Tony Morris :

>>>>>>>>

>>>>>>>>

>>>>>>>>

>>>>>>>>

>>>>>>>>> It's entirely possible to construct a de-facto world state. The

>>>>>>>>> signature definitely does have just one instance. It definitely does.

>>>>>>>>> There is a proof. The strongest possible claim about reality exists.

>>>>>>>>> There's not much I can do about the fact that you are refuting a proof

>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's

>>>>>>>>> not even a debate.

>>>>>>>>>

>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well

>>>>>>>>> aware that Scala does not have an effect system. The question arises,

>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already

>>>>>>>>> made this point -- *I* have already made this point.

>>>>>>>>>

>>>>>>>>> I will repeat myself:

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

>>>>>>>>>

>>>>>>>>> No subverting the types, assume termination --> once-inhabited!

>>>>>>>>>

>>>>>>>>> I am exhausted, you win.

>>>>>>>>>

>>>>>>>>> Dimitris Andreou wrote:

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>> 2009/11/13 Tony Morris :

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>> Rex,

>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is

>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well

>>>>>>>>>>> understood basic fact of computational theory.

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>> The problem is that a signature never captures the implicit "world"

>>>>>>>>>> argument that all functions have (otherwise, please show me your

>>>>>>>>>> functions having the "world" argument from which you access all of

>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one

>>>>>>>>>> instance, but infinitely many.

>>>>>>>>>>

>>>>>>>>>> If you don't assume that a function is able to compute other

>>>>>>>>>> functions, just because it didn't have them as arguments, you talk

>>>>>>>>>> about something else but definitely not about scala programming. May I

>>>>>>>>>> remind that the discussion is about _scala_ docs.

>>>>>>>>>>

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

>>>>>>>>>>

>>>>>>>>>> Regards,

>>>>>>>>>> Dimitris

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A

>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard

>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them

>>>>>>>>>>> with -> symbol.

>>>>>>>>>>>

>>>>>>>>>>> Let's draw the truth table for implication:

>>>>>>>>>>> P Q P->Q

>>>>>>>>>>> 0 0 1

>>>>>>>>>>> 0 1 1

>>>>>>>>>>> 1 0 0

>>>>>>>>>>> 1 1 1

>>>>>>>>>>>

>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that

>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a

>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a

>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"

>>>>>>>>>>>

>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One

>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does

>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The

>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."

>>>>>>>>>>>

>>>>>>>>>>> The question can be phrased in English as "tell the truth about this

>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,

>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the

>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our

>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).

>>>>>>>>>>>

>>>>>>>>>>> I really hope this helps. This is exhausting.

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>> Rex Kerr wrote:

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>> Tony,

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

>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,

>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.

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

>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say

>>>>>>>>>>>> exactly what the return type should be for the Double square

>>>>>>>>>>>> function. If the return type for the Double function is not Double,

>>>>>>>>>>>> please explain what the return type is for the F(n) function which

>>>>>>>>>>>> computes the n'th Fibonacci number.

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

>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate

>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing

>>>>>>>>>>>> on the basis of solid principles.

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

>>>>>>>>>>>> (Or, of course, we can just drop it.)

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

>>>>>>>>>>>> --Rex

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

>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>> > wrote:

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

>>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.

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

>>>>>>>>>>>> I assure you, there is only one possible solution and I didn't

>>>>>>>>>>>> just make

>>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I

>>>>>>>>>>>> predict we wouldn't be having this discussion, but a more

>>>>>>>>>>>> interesting one.

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

>>>>>>>>>>>> Rex Kerr wrote:

>>>>>>>>>>>> > There are infinitely many possible answers to what can happen with

>>>>>>>>>>>> > that type signature, given that A and B can be any type. What

>>>>>>>>>>>> if foo

>>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while

>>>>>>>>>>>> leaving

>>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a

>>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about

>>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that

>>>>>>>>>>>> > might have practical utility.

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

>>>>>>>>>>>> > For example,

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

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

>>>>>>>>>>>> > new (a:A) => (c:C) {

>>>>>>>>>>>> > val b = f(a)

>>>>>>>>>>>> > g(

>>>>>>>>>>>> > b match {

>>>>>>>>>>>> > case x:Int : -x

>>>>>>>>>>>> > case x:Long : -x

>>>>>>>>>>>> > case x:Float : -x

>>>>>>>>>>>> > case x:Double: -x

>>>>>>>>>>>> > case y: y

>>>>>>>>>>>> > }

>>>>>>>>>>>> > )

>>>>>>>>>>>> > }

>>>>>>>>>>>> > }

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

>>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get

>>>>>>>>>>>> the idea.)

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

>>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly

>>>>>>>>>>>> what is

>>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly

>>>>>>>>>>>> what is

>>>>>>>>>>>> > promised.

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

>>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had

>>>>>>>>>>>> one-to-one

>>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to

>>>>>>>>>>>> > handle. (Unless, of course, you think that def

>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for

>>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type

>>>>>>>>>>>> > system is impractical.)

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

>>>>>>>>>>>> > --Rex

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

>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris

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

>>>>>>>>>>>> > >> wrote:

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

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

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

>>>>>>>>>>>> > print

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

>>>>>>>>>>>> legacy.

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

>>>>>>>>>>>> > There is only *one possible answer*.

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

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

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

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

>>>>>>>>>>>> Tony Morris

>>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

>>>>>>>>>>> Tony Morris

>>>>>>>>>>> http://tmorris.net/

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>> --

>>>>>>>>> Tony Morris

>>>>>>>>> http://tmorris.net/

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>> --

>>>>>>> Tony Morris

>>>>>>> http://tmorris.net/

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>> --

>>>>> Tony Morris

>>>>> http://tmorris.net/

>>>>>

>>>>>

>>>>>

>>>>>

>>>>>

>>>>

>>> --

>>> Tony Morris

>>> http://tmorris.net/

>>>

>>>

>>>

>>>

>>

>>

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 02:37

#56
Re: Scaladoc that is actually useful?

Still need some language (e.g. english) to describe these assumptions.

They are not axioms you know or theorems, they

are...argh...assumptions. Please document your assumptions! Please ask

students to document their assumptions :)

2009/11/13 Tony Morris :

> No, the existence of these assumptions (finally!) does not justify the

> use of English for the general case.

>

> Dimitris Andreou wrote:

>> Alright, I think we can finally agree and end this peacefully. The

>> signature *plus* some assumptions (encoded in perfectly good english)

>> may make it once-habitated. The scala signature itself does _not_,

>> since it does not by itself provide any extra assumptions. Many of us

>> thought perhaps misunderstood that you were saying that the latter is

>> also once-habitated by itself, so no english were needed in the

>> scaladocs - while they *are* needed to make this extra claim, thus the

>> debate. End of story. Is that ok with you?

>>

>> 2009/11/13 Tony Morris :

>>

>>> Please don't be dishonest. This is the *fourth time*.

>>>

>>> Let's restate the assumptions:

>>>

>>> * Assume termination

>>> * No subverting the types

>>>

>>> Dimitris Andreou wrote:

>>>

>>>> 2009/11/13 Tony Morris :

>>>>

>>>>

>>>>> Actually, I didn't claim that at all.

>>>>>

>>>>>

>>>> Erm... "I assure you, the signature given is once-inhabited" - and you

>>>> kind of insisted that you were talking about scala...

>>>>

>>>>

>>>>

>>>>> For the fourth time...

>>>>>

>>>>> ah bugger it. And no, the halting problem does not contradict that at

>>>>> all (ugh!).

>>>>>

>>>>>

>>>> But you are right about that, of course. It doesn't take a halting

>>>> problem to prove that there are non-terminating implementations (which

>>>> simultaneously conform to the supposedly once-habitated signature

>>>> though!), one can just create a trivial example.

>>>>

>>>> Bye!

>>>>

>>>>

>>>>> Dimitris Andreou wrote:

>>>>>

>>>>>

>>>>>> Since *you* claimed that there was only a single implementation of

>>>>>> that signature, it is *you* that imply that all possible

>>>>>> implementations are halting. Guess what, that's exactly what the

>>>>>> halting problem contradicts :)

>>>>>>

>>>>>> See you! It was fun :)

>>>>>> I really like you you know, but sometimes I think you just rant

>>>>>> unchecked (with no suppress compiler option :) )

>>>>>>

>>>>>> Good night all,

>>>>>> Dimitris

>>>>>>

>>>>>> 2009/11/13 Tony Morris :

>>>>>>

>>>>>>

>>>>>>

>>>>>>> "I am not discussing this matter any further until you have solved the

>>>>>>> turing halting problem!"

>>>>>>>

>>>>>>> That's fine by me, I'm exhausted :) Seeya!

>>>>>>>

>>>>>>> Dimitris Andreou wrote:

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>> Omg, you used...english! Please encode these constrains as a scala

>>>>>>>> signature and I go home. :)

>>>>>>>>

>>>>>>>> 2009/11/13 Tony Morris :

>>>>>>>>

>>>>>>>>

>>>>>>>>

>>>>>>>>

>>>>>>>>> You seem to have overlooked some important parts. I will repeat them for

>>>>>>>>> a third time:

>>>>>>>>>

>>>>>>>>> * No subverting the types

>>>>>>>>> * Assume termination

>>>>>>>>>

>>>>>>>>> *crosses fingers*

>>>>>>>>>

>>>>>>>>> Dimitris Andreou wrote:

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>> 2009/11/13 Tony Morris :

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

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

>>>>>>>>>>> see that.

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>> I hope that was *not* your favourite line as a lecturer :)

>>>>>>>>>>

>>>>>>>>>> This is the signature I see you gave:

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

>>>>>>>>>>

>>>>>>>>>> It does not constrain "boo" (scala) implementations from using the

>>>>>>>>>> implicit world. So you did not address my request. If you gave another

>>>>>>>>>> signature I missed, please repeat.

>>>>>>>>>>

>>>>>>>>>> Dimitris

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>>> Dimitris Andreou wrote:

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>> As I said, please give us a scala signature that constrains its body

>>>>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how

>>>>>>>>>>>> exactly you encode the mathematical signature into a scala signature

>>>>>>>>>>>> which also has just one implementation. Thank you.

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

>>>>>>>>>>>> 2009/11/13 Tony Morris :

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

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

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

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

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

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

>>>>>>>>>>>>> It's entirely possible to construct a de-facto world state. The

>>>>>>>>>>>>> signature definitely does have just one instance. It definitely does.

>>>>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.

>>>>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof

>>>>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's

>>>>>>>>>>>>> not even a debate.

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

>>>>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well

>>>>>>>>>>>>> aware that Scala does not have an effect system. The question arises,

>>>>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already

>>>>>>>>>>>>> made this point -- *I* have already made this point.

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

>>>>>>>>>>>>> I will repeat myself:

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

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

>>>>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!

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

>>>>>>>>>>>>> I am exhausted, you win.

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

>>>>>>>>>>>>> Dimitris Andreou wrote:

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

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

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

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

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

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

>>>>>>>>>>>>>> 2009/11/13 Tony Morris :

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

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

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

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

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

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

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

>>>>>>>>>>>>>>> Rex,

>>>>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is

>>>>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well

>>>>>>>>>>>>>>> understood basic fact of computational theory.

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

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

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

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

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

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

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

>>>>>>>>>>>>>> The problem is that a signature never captures the implicit "world"

>>>>>>>>>>>>>> argument that all functions have (otherwise, please show me your

>>>>>>>>>>>>>> functions having the "world" argument from which you access all of

>>>>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one

>>>>>>>>>>>>>> instance, but infinitely many.

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

>>>>>>>>>>>>>> If you don't assume that a function is able to compute other

>>>>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk

>>>>>>>>>>>>>> about something else but definitely not about scala programming. May I

>>>>>>>>>>>>>> remind that the discussion is about _scala_ docs.

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

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

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

>>>>>>>>>>>>>> Regards,

>>>>>>>>>>>>>> Dimitris

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

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

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

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

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

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

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

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

>>>>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A

>>>>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard

>>>>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them

>>>>>>>>>>>>>>> with -> symbol.

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

>>>>>>>>>>>>>>> Let's draw the truth table for implication:

>>>>>>>>>>>>>>> P Q P->Q

>>>>>>>>>>>>>>> 0 0 1

>>>>>>>>>>>>>>> 0 1 1

>>>>>>>>>>>>>>> 1 0 0

>>>>>>>>>>>>>>> 1 1 1

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

>>>>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that

>>>>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a

>>>>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a

>>>>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"

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

>>>>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One

>>>>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does

>>>>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The

>>>>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."

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

>>>>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this

>>>>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,

>>>>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the

>>>>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our

>>>>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).

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

>>>>>>>>>>>>>>> I really hope this helps. This is exhausting.

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

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

>>>>>>>>>>>>>>> Rex Kerr wrote:

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

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

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

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

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

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

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

>>>>>>>>>>>>>>>> Tony,

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

>>>>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,

>>>>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.

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

>>>>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say

>>>>>>>>>>>>>>>> exactly what the return type should be for the Double square

>>>>>>>>>>>>>>>> function. If the return type for the Double function is not Double,

>>>>>>>>>>>>>>>> please explain what the return type is for the F(n) function which

>>>>>>>>>>>>>>>> computes the n'th Fibonacci number.

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

>>>>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate

>>>>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing

>>>>>>>>>>>>>>>> on the basis of solid principles.

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

>>>>>>>>>>>>>>>> (Or, of course, we can just drop it.)

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

>>>>>>>>>>>>>>>> --Rex

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

>>>>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>>>>> > wrote:

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

>>>>>>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.

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

>>>>>>>>>>>>>>>> I assure you, there is only one possible solution and I didn't

>>>>>>>>>>>>>>>> just make

>>>>>>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I

>>>>>>>>>>>>>>>> predict we wouldn't be having this discussion, but a more

>>>>>>>>>>>>>>>> interesting one.

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

>>>>>>>>>>>>>>>> Rex Kerr wrote:

>>>>>>>>>>>>>>>> > There are infinitely many possible answers to what can happen with

>>>>>>>>>>>>>>>> > that type signature, given that A and B can be any type. What

>>>>>>>>>>>>>>>> if foo

>>>>>>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while

>>>>>>>>>>>>>>>> leaving

>>>>>>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a

>>>>>>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about

>>>>>>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that

>>>>>>>>>>>>>>>> > might have practical utility.

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

>>>>>>>>>>>>>>>> > For example,

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

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

>>>>>>>>>>>>>>>> > new (a:A) => (c:C) {

>>>>>>>>>>>>>>>> > val b = f(a)

>>>>>>>>>>>>>>>> > g(

>>>>>>>>>>>>>>>> > b match {

>>>>>>>>>>>>>>>> > case x:Int : -x

>>>>>>>>>>>>>>>> > case x:Long : -x

>>>>>>>>>>>>>>>> > case x:Float : -x

>>>>>>>>>>>>>>>> > case x:Double: -x

>>>>>>>>>>>>>>>> > case y: y

>>>>>>>>>>>>>>>> > }

>>>>>>>>>>>>>>>> > )

>>>>>>>>>>>>>>>> > }

>>>>>>>>>>>>>>>> > }

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

>>>>>>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get

>>>>>>>>>>>>>>>> the idea.)

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

>>>>>>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly

>>>>>>>>>>>>>>>> what is

>>>>>>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly

>>>>>>>>>>>>>>>> what is

>>>>>>>>>>>>>>>> > promised.

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

>>>>>>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had

>>>>>>>>>>>>>>>> one-to-one

>>>>>>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to

>>>>>>>>>>>>>>>> > handle. (Unless, of course, you think that def

>>>>>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for

>>>>>>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type

>>>>>>>>>>>>>>>> > system is impractical.)

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

>>>>>>>>>>>>>>>> > --Rex

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

>>>>>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris

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

>>>>>>>>>>>>>>>> > >> wrote:

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

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

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

>>>>>>>>>>>>>>>> > print

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

>>>>>>>>>>>>>>>> legacy.

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

>>>>>>>>>>>>>>>> > There is only *one possible answer*.

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

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

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

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

>>>>>>>>>>>>>>>> Tony Morris

>>>>>>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

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

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

>>>>>>>>>>>>>>> Tony Morris

>>>>>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

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

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

>>>>>>>>>>>>> Tony Morris

>>>>>>>>>>>>> http://tmorris.net/

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

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

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

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

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

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

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

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

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

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

>>>>>>>>>>> Tony Morris

>>>>>>>>>>> http://tmorris.net/

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>> --

>>>>>>>>> Tony Morris

>>>>>>>>> http://tmorris.net/

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>>>>

>>>>>>> --

>>>>>>> Tony Morris

>>>>>>> http://tmorris.net/

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>> --

>>>>> Tony Morris

>>>>> http://tmorris.net/

>>>>>

>>>>>

>>>>>

>>>>>

>>>>>

>>>>

>>> --

>>> Tony Morris

>>> http://tmorris.net/

>>>

>>>

>>>

>>>

>>

>>

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 02:37

#57
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:

> Termination is an axiom? :-/

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

Randall Schulz

Fri, 2009-11-13, 02:47

#58
Re: Scaladoc that is actually useful?

Well, I think we understand how there is only one definition of

def func[A, B, C](f1: A=>B, f2: B=>C): A=>C

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

Best regards,

Brian Maso

(949) 395-8551

brian [at] blumenfeld-maso [dot] com

twitter: @bmaso

skype: brian.maso

LinkedIn: http://www.linkedin.com/in/brianmaso

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

def func[A, B, C](f1: A=>B, f2: B=>C): A=>C

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

Best regards,

Brian Maso

(949) 395-8551

brian [at] blumenfeld-maso [dot] com

twitter: @bmaso

skype: brian.maso

LinkedIn: http://www.linkedin.com/in/brianmaso

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

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

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

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

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

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

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

for it!), Types as Theorems.

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

Theorems.

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

outcome. Hopefully the silent audience did some thinking!

christopher marshall wrote:

> How does a function:

>

> def foo(i: Int) : String

>

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

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

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

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

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

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

>

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

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

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

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

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

> >

> >

> >

> > christopher marshall wrote:

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

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

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

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

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

> >

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

> Isomorphism.

> >

> > --

> > Tony Morris

> > http://tmorris.net/

> >

> >

>

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

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

> accounts. Find out how. <http://clk.atdmt.com/UKM/go/186394592/direct/01/>

--

Tony Morris

http://tmorris.net/

Fri, 2009-11-13, 02:57

#59
Re: Scaladoc that is actually useful?

Fri, 2009-11-13, 03:17

#60
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Dimitris Andreou wrote:

> Not in scala functions/signatures though, that was the confusion of

> all this debate :) anyway, not to create a mini-private-debate. I'm

> out, good night!

You have to realize that when a method computes something at odds with

its signature, that method is buggy.

Randall Schulz

Fri, 2009-11-13, 03:57

#61
Re: Scaladoc that is actually useful?

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

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

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

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

It seems highly impractical, however, from a code duplication standpoint to never allow a generic function to understand something about the types that are thrown at it. So, yes, nice elegance, yay, but if I am going to program something, I don't want to have to write my composition function over again _in its entirety_ for Int, Float, Double, Long, whatever, just so that I keep the type signature conforming to the "functions only import the mathematics of their arguments" rule.

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

For example,

f(x) : R -> R = {

x == 0 : 0

x in Z : 1/x

else: x

}

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

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

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

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

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

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

--Rex

Functions are self-contained and pure. They know not of the world, other

than that portion of the world of mathematics that defines them.

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

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

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

It seems highly impractical, however, from a code duplication standpoint to never allow a generic function to understand something about the types that are thrown at it. So, yes, nice elegance, yay, but if I am going to program something, I don't want to have to write my composition function over again _in its entirety_ for Int, Float, Double, Long, whatever, just so that I keep the type signature conforming to the "functions only import the mathematics of their arguments" rule.

Programmers have repeatedly been guilty of butchering established

concepts and terminology. Calling something a function that does not

conform to the definition of function universally agreed upon by

mathematicians is inexcusable.

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

For example,

f(x) : R -> R = {

x == 0 : 0

x in Z : 1/x

else: x

}

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

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

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

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

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

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

--Rex

Fri, 2009-11-13, 04:07

#62
Re: Scaladoc that is actually useful?

Tony Morris-4 wrote:

>

> Do you know what function means?

>

In type theory? In intuitionistic (a.k.a constructive) type theory? In

recursive function theory? In Haskell? In Scala? In C?

Yes, I know what 'function' means, in all of the above. Even though the

definitions there have almost as many differences as similarities.

In "reality"? Oh, hell no! I certainly don't know what a function is in

"reality", but based on the disagreement on this point among philosophers of

mathematics I'm pretty sure I'm not alone. The one thing I am sure of is

that it's not the sort of naive Platonism you seem to be espousing. If I

take a rock and sift it down to constituent quarks I'm pretty certain I

won't see any functions.

How exactly is this helpful to someone who is trying to get some work done

and complaining that someone else didn't write good doc?

--Dave Griffith

Fri, 2009-11-13, 04:27

#63
Re: Scaladoc that is actually useful?

So er, back to reality.

Can you provide two inhabitants for:

forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

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

Dave Griffith wrote:

>

>

> Tony Morris-4 wrote:

>

>> Do you know what function means?

>>

>>

>

> In type theory? In intuitionistic (a.k.a constructive) type theory? In

> recursive function theory? In Haskell? In Scala? In C?

>

> Yes, I know what 'function' means, in all of the above. Even though the

> definitions there have almost as many differences as similarities.

>

> In "reality"? Oh, hell no! I certainly don't know what a function is in

> "reality", but based on the disagreement on this point among philosophers of

> mathematics I'm pretty sure I'm not alone. The one thing I am sure of is

> that it's not the sort of naive Platonism you seem to be espousing. If I

> take a rock and sift it down to constituent quarks I'm pretty certain I

> won't see any functions.

>

> How exactly is this helpful to someone who is trying to get some work done

> and complaining that someone else didn't write good doc?

>

> --Dave Griffith

>

>

Fri, 2009-11-13, 04:47

#64
Re: Scaladoc that is actually useful?

Tony, I think you've quite adequately put the point across that

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

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

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

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

Ishaaq

2009/11/13 Tony Morris <tonymorris [at] gmail [dot] com>

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

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

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

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

Ishaaq

2009/11/13 Tony Morris <tonymorris [at] gmail [dot] com>

So er, back to reality.

Can you provide two inhabitants for:

forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

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

Dave Griffith wrote:

>

>

> Tony Morris-4 wrote:

>

>> Do you know what function means?

>>

>>

>

> In type theory? In intuitionistic (a.k.a constructive) type theory? In

> recursive function theory? In Haskell? In Scala? In C?

>

> Yes, I know what 'function' means, in all of the above. Even though the

> definitions there have almost as many differences as similarities.

>

> In "reality"? Oh, hell no! I certainly don't know what a function is in

> "reality", but based on the disagreement on this point among philosophers of

> mathematics I'm pretty sure I'm not alone. The one thing I am sure of is

> that it's not the sort of naive Platonism you seem to be espousing. If I

> take a rock and sift it down to constituent quarks I'm pretty certain I

> won't see any functions.

>

> How exactly is this helpful to someone who is trying to get some work done

> and complaining that someone else didn't write good doc?

>

> --Dave Griffith

>

>

--

Tony Morris

http://tmorris.net/

Fri, 2009-11-13, 04:57

#65
Re: Scaladoc that is actually useful?

Hello Ishaaq,

If I have adequately conveyed a point that is provable, has been proven

(by parametricity) and is easily falsifiable, then you'd think I'd hit

less resistance., but alas, it appears not.

I think I have adequately answered your concluding question too, don't

you? For those signatures that are inhabited more than once (and yes,

there are a lot), what should we do? The rash conclusion of "write

English" is just that, rash and has about as much thought put into it as

many of the respondents have put into my original question (hence, the

laborious repetition). My answer has thus far been, "No I am not (yet)

claiming anything about function signatures with multiple inhabitants."

I haven't even got to the point of being able to examine your question

further -- instead, we are going over and over on a matter of fact as if

it is even debatable! I was hoping that once this observation was made

(that there exists a signature for which documentation/tests are

redundant), then we could raise further questions. Ah, the Scala

community :)

It has been suggested to me by two peers that I should "bash them over

the head" but I still hold hope for a productive outcome!

Ishaaq Chandy wrote:

> Tony, I think you've quite adequately put the point across that

>

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

>

> has only one truthful inhabitant and should quite legitimately be left

> undocumented. It could be argued that it is the onus of a programmer

> who writes an untruthful implementation of that function to document

> it instead of asking that the truthful one be documented.

>

> Yet, I think this function has been raised as a straw-man. A large

> percentage of function signatures don't have the luxury of having only

> one inhabitant. I haven't really sat down and counted the number of

> such functions in the scala library that have not been documented. Nor

> have I counted the number side-affecting *methods* (as opposed to real

> functions) in the scala library that are undocumented, but my

> conjecture (happy for it to be proved wrong) is that those numbers are

> large enough to be concerned about. Which is what, IMO, the OP was

> concerned about.

>

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

> documented?

>

> Ishaaq

>

> 2009/11/13 Tony Morris >

>

> So er, back to reality.

>

> Can you provide two inhabitants for:

> forall A B C. (A => B) => (B => C) => A => C

>

> Assume termination and no lies.

>

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

>

> Dave Griffith wrote:

> >

> >

> > Tony Morris-4 wrote:

> >

> >> Do you know what function means?

> >>

> >>

> >

> > In type theory? In intuitionistic (a.k.a constructive) type

> theory? In

> > recursive function theory? In Haskell? In Scala? In C?

> >

> > Yes, I know what 'function' means, in all of the above. Even

> though the

> > definitions there have almost as many differences as similarities.

> >

> > In "reality"? Oh, hell no! I certainly don't know what a

> function is in

> > "reality", but based on the disagreement on this point among

> philosophers of

> > mathematics I'm pretty sure I'm not alone. The one thing I am

> sure of is

> > that it's not the sort of naive Platonism you seem to be

> espousing. If I

> > take a rock and sift it down to constituent quarks I'm pretty

> certain I

> > won't see any functions.

> >

> > How exactly is this helpful to someone who is trying to get some

> work done

> > and complaining that someone else didn't write good doc?

> >

> > --Dave Griffith

> >

> >

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 05:17

#66
Re: Scaladoc that is actually useful?

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

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

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

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

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

--Rex

Hello Ishaaq,

If I have adequately conveyed a point that is provable, has been proven

(by parametricity) and is easily falsifiable, then you'd think I'd hit

less resistance., but alas, it appears not.

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

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

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

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

--Rex

Fri, 2009-11-13, 05:17

#67
Re: Scaladoc that is actually useful?

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

I was not assuming anything more than what I stated. Please (at least)

read Theorems for Free, Wadler. Or, if you like take the issue up with

the author of the @free plugin, which, knowingly or not, *proved*

(that's proved) the point way back.

Rex Kerr wrote:

> On Thu, Nov 12, 2009 at 10:52 PM, Tony Morris > wrote:

>

> Hello Ishaaq,

> If I have adequately conveyed a point that is provable, has been

> proven

> (by parametricity) and is easily falsifiable, then you'd think I'd hit

> less resistance., but alas, it appears not.

>

>

> You would have had a much easier time if you had stated up-front that

> you were assuming constructive type theory (or whatever it is that

> you're actually assuming--you never quite made that clear, though I

> believe constructive type theory fits), and that you assume that the

> basic terminology and results of type theory should be a prerequisite

> for anyone using Scala, and that one should only use Scala in ways

> consistent with type theory (even though it admits other patterns).

>

> Actually, I don't know if you would have had an easier time, but with

> that as an assumption about what you meant, yes, what you're saying

> appears to be proven true--not much room for argument there.

>

> Except I don't think that a signature that is proof of its function

> _by constructive type theory_ should necessarily be undocumented in

> Scala. If you write a library consisting entirely of stuff useful

> only to people working on constructive type theory, then I absolutely

> agree that the signature is plenty.

>

> Otherwise, you might want to explain what you're doing in a comment on

> the method. At least something like "Obeys all assumptions of

> constructive type theory."

>

> --Rex

>

Fri, 2009-11-13, 05:27

#68
Re: Scaladoc that is actually useful?

I think you meant two different inhabitants that are not reducible to each other, don't you? I mean, the following are equivalent, but different "functions" (your meaning) of the signature "def func[A, B, C](f1: A => B, f2: B => C): A => C"

// keeping it simple

return f2(f1(a));

// bwahahaha

val x = true;

return if(x) { f2(f1(a)) } else { null }

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

Best regards,

Brian Maso

(949) 395-8551

brian [at] blumenfeld-maso [dot] com

twitter: @bmaso

skype: brian.maso

LinkedIn: http://www.linkedin.com/in/brianmaso

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

// keeping it simple

return f2(f1(a));

// bwahahaha

val x = true;

return if(x) { f2(f1(a)) } else { null }

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

Best regards,

Brian Maso

(949) 395-8551

brian [at] blumenfeld-maso [dot] com

twitter: @bmaso

skype: brian.maso

LinkedIn: http://www.linkedin.com/in/brianmaso

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

So er, back to reality.

Can you provide two inhabitants for:

forall A B C. (A => B) => (B => C) => A => C

Assume termination and no lies.

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

Dave Griffith wrote:

>

>

> Tony Morris-4 wrote:

>

>> Do you know what function means?

>>

>>

>

> In type theory? In intuitionistic (a.k.a constructive) type theory? In

> recursive function theory? In Haskell? In Scala? In C?

>

> Yes, I know what 'function' means, in all of the above. Even though the

> definitions there have almost as many differences as similarities.

>

> In "reality"? Oh, hell no! I certainly don't know what a function is in

> "reality", but based on the disagreement on this point among philosophers of

> mathematics I'm pretty sure I'm not alone. The one thing I am sure of is

> that it's not the sort of naive Platonism you seem to be espousing. If I

> take a rock and sift it down to constituent quarks I'm pretty certain I

> won't see any functions.

>

> How exactly is this helpful to someone who is trying to get some work done

> and complaining that someone else didn't write good doc?

>

> --Dave Griffith

>

>

--

Tony Morris

http://tmorris.net/

Fri, 2009-11-13, 05:27

#69
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:

> On Thu, Nov 12, 2009 at 7:25 PM, Randall R Schulz wrote:

> > Functions are self-contained and pure. They know not of the world,

> > other than that portion of the world of mathematics that defines

> > them.

>

> ...

>

> It seems highly impractical, however, from a code duplication

> standpoint to never allow a generic function to understand something

> about the types that are thrown at it.

Then the signature exhibits those type constraints.

> So, yes, nice elegance, yay,

> but if I am going to program something, I don't want to have to write

> my composition function over again _in its entirety_ for Int, Float,

> Double, Long, whatever, just so that I keep the type signature

> conforming to the "functions only import the mathematics of their

> arguments" rule.

There's no need. Scala accommodates a single source

for our now classic function composition:

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

compose: [A,B,C]((A) => B,(B) => C)(A) => C

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

i2f: (Int)Float

scala> val i2fF = i2f _

i2fF: (Int) => Float =

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

f2s: (Float)String

scala> val f2sF = f2s _

f2sF: (Float) => String =

scala> val i2sF = compose(i2f, f2s)

i2sF: (Int) => String =

scala> i2sF(2)

res0: String = 2.0

> > Programmers have repeatedly been guilty of butchering established

> > concepts and terminology. Calling something a function that does

> > not conform to the definition of function universally agreed upon

> > by mathematicians is inexcusable.

>

> This is absolutely not the definition of function "universally agreed

> upon by mathematicians".

>

> For example,

>

> f(x) : R -> R = {

> x == 0 : 0

> x in Z : 1/x

> else: x

> }

>

> is a perfectly well-defined function on the reals, and it knows all

> about integers which is disallowed by the "pure" function definition

> above.

Where does that function use information outside its definition to alter

what it computes?

> ...

>

> --Rex

Randall Schulz

Fri, 2009-11-13, 05:37

#70
Re: Scaladoc that is actually useful?

No, null represents a logical absurdity (non-termination). I think you

mean the body of the function may look syntactically different. This may

well be.

Brian Maso wrote:

> I think you meant two different inhabitants that are not reducible to

> each other, don't you? I mean, the following are equivalent, but

> different "functions" (your meaning) of the signature "def func[A, B,

> C](f1: A => B, f2: B => C): A => C"

>

> // keeping it simple

> return f2(f1(a));

>

> // bwahahaha

> val x = true;

> return if(x) { f2(f1(a)) } else { null }

>

> or some other such nonsense reducible to the simple implementation a

> by sequence of refactorings.

>

> Best regards,

> Brian Maso

> (949) 395-8551

> brian [at] blumenfeld-maso [dot] com

> twitter: @bmaso

> skype: brian.maso

> LinkedIn: http://www.linkedin.com/in/brianmaso

>

> On Thu, Nov 12, 2009 at 7:22 PM, Tony Morris > wrote:

>

> So er, back to reality.

>

> Can you provide two inhabitants for:

> forall A B C. (A => B) => (B => C) => A => C

>

> Assume termination and no lies.

>

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

>

> Dave Griffith wrote:

> >

> >

> > Tony Morris-4 wrote:

> >

> >> Do you know what function means?

> >>

> >>

> >

> > In type theory? In intuitionistic (a.k.a constructive) type

> theory? In

> > recursive function theory? In Haskell? In Scala? In C?

> >

> > Yes, I know what 'function' means, in all of the above. Even

> though the

> > definitions there have almost as many differences as similarities.

> >

> > In "reality"? Oh, hell no! I certainly don't know what a

> function is in

> > "reality", but based on the disagreement on this point among

> philosophers of

> > mathematics I'm pretty sure I'm not alone. The one thing I am

> sure of is

> > that it's not the sort of naive Platonism you seem to be

> espousing. If I

> > take a rock and sift it down to constituent quarks I'm pretty

> certain I

> > won't see any functions.

> >

> > How exactly is this helpful to someone who is trying to get some

> work done

> > and complaining that someone else didn't write good doc?

> >

> > --Dave Griffith

> >

> >

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 05:57

#71
Re: Scaladoc that is actually useful?

Earlier today I agreed with the original poster that there is a

problem with Scaladoc, in that it makes seemingly simple tasks

excessively complex for the programmer who has to get work done. That

discussion went off on some odd tangent about type systems that I will

ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer

in 2.8. The scaladoc sends me to

ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

SeqLike

PartialFunction

Function1

iterableLike

GenericTraversableTemplate

TraversableLike

AnyRef

Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

But then the Scaladoc could have a friendlier way of helping the new

user, such as inline expanding the docs for the traits, or at least,

copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother

knows more type theory than your mother".

Fri, 2009-11-13, 05:57

#72
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:

> On Thu, Nov 12, 2009 at 11:21 PM, Randall R Schulz wrote:

>

> > > ... I don't want to have to

> > > write my composition function over again _in its entirety_ for

> > > Int, Float, Double, Long, whatever, just so that I keep the type

> > > signature conforming to the "functions only import the

> > > mathematics of their arguments" rule.

> >

> > There's no need. Scala accommodates a single source

> > for our now classic function composition:

>

> That's nice, except my example inverted the sign of numeric inputs by

> matching on the type of the return value of f. Your example doesn't

> do that. What if I want to do that without lots of code duplication?

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

here):

> > > ... I don't want to have to

> > > write my composition function over again _in its entirety_ for

> > > Int, Float, Double, Long, whatever

A Scala implementation of your f(x: R): R would compose using the

compose function I showed, assuming a representation of R that meets

whatever criteria you have (obviously floating-point only approximates

the reals).

> ...

> >

> > Where does that function use information outside its definition to

> > alter what it computes?

>

> The reals need not know anything about the integers. ...

>

> Another thing a mathematical function could do ..

I don't know how you read my words, but all these things are functions

that do not use external state to condition what they compute. They are

self-contained, pure functions.

> --Rex

Randall Schulz

Fri, 2009-11-13, 06:07

#73
Re: Scaladoc that is actually useful?

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

That's nice, except my example inverted the sign of numeric inputs by matching on the type of the return value of f. Your example doesn't do that. What if I want to do that without lots of code duplication?

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

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

--Rex

> So, yes, nice elegance, yay,

> but if I am going to program something, I don't want to have to write

> my composition function over again _in its entirety_ for Int, Float,

> Double, Long, whatever, just so that I keep the type signature

> conforming to the "functions only import the mathematics of their

> arguments" rule.

There's no need. Scala accommodates a single source

for our now classic function composition:

That's nice, except my example inverted the sign of numeric inputs by matching on the type of the return value of f. Your example doesn't do that. What if I want to do that without lots of code duplication?

> > Programmers have repeatedly been guilty of butchering established

> > concepts and terminology. Calling something a function that does

> > not conform to the definition of function universally agreed upon

> > by mathematicians is inexcusable.

>

> This is absolutely not the definition of function "universally agreed

> upon by mathematicians".

>

> For example,

>

> f(x) : R -> R = {

> x == 0 : 0

> x in Z : 1/x

> else: x

> }

>

> is a perfectly well-defined function on the reals, and it knows all

> about integers which is disallowed by the "pure" function definition

> above.

Where does that function use information outside its definition to alter

what it computes?

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

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

--Rex

Fri, 2009-11-13, 06:07

#74
Re: Scaladoc that is actually useful?

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

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

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

(a:A) => {

val b = f(a)

g(

b match {

case x:Int => -x

case x:Long => -x

case x:Float => -x

case x:Double => -x

case y => y

}

)

}

}

which absolutely obeys the types _viewed as sets_. I have constructed a function that, for each input in the set

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

produces an element in the set

(A=>C)

which is what is required of a mathematical function.

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

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

--Rex

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

here):

> > > ... I don't want to have to

> > > write my composition function over again _in its entirety_ for

> > > Int, Float, Double, Long, whatever

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

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

(a:A) => {

val b = f(a)

g(

b match {

case x:Int => -x

case x:Long => -x

case x:Float => -x

case x:Double => -x

case y => y

}

)

}

}

which absolutely obeys the types _viewed as sets_. I have constructed a function that, for each input in the set

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

produces an element in the set

(A=>C)

which is what is required of a mathematical function.

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

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

--Rex

Fri, 2009-11-13, 06:17

#75
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Cay Horstmann wrote:

> Earlier today I agreed with the original poster that there is a

> problem with Scaladoc, in that it makes seemingly simple tasks

> excessively complex for the programmer who has to get work done. ...

>

> suppose I want to use an ArrayBuffer in 2.8. The scaladoc sends me to

>

> ResizableArray

> Builder

> ...

> AnyRef

> Any

>

> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

> But then the Scaladoc could have a friendlier way of helping the new

> user, such as inline expanding the docs for the traits, or at least,

> copying out the summary method statements.

The Scaladoc HTML is an API reference, not a tutorial. Answers to "how

do I accomplish X" questions don't really belong there, I don't think.

> This really needs some fresh thinking without detours into "my mother

> knows more type theory than your mother".

A comprehensive tutorial introduction to its collection classes, e.g.,

is surely called for. I'm not sure to what extent that qualifies as

fresh thinking, though.

Scala is underdocumented, to be sure. Scarcely any open-source or

academic project at a comparable stage of evolution is.

Randall Schulz

Fri, 2009-11-13, 07:27

#76
Re: Scaladoc that is actually useful?

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

> (a:A) => {

> val b = f(a)

> g(

> b match {

> case x:Int => -x

> case x:Long => -x

> case x:Float => -x

> case x:Double => -x

> case y => y

> }

> )

> }

> }

>

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

Fri, 2009-11-13, 07:37

#77
Re: Scaladoc that is actually useful?

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

>

Oh, and Scala even gives you a type error:

error: type mismatch;

found : Int

required: B

case x:Int => -x

Good on ya, Scala.

Fri, 2009-11-13, 07:37

#78
Re: Scaladoc that is actually useful?

I addressed that issue earlier. It's called a type case (see

Data.Typeable). It is indeed a lie (forall A B. A -> B) i.e. the cast

operation.

It is safe to conclude that the proven fact is still indeed a proven

fact and you all have nothing to worry about.

Randall R Schulz wrote:

> On Thursday November 12 2009, Rex Kerr wrote:

>

>> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:

>>

>>> You're moving the target. I addressed your statement above (copied

>>>

>>> here):

>>>

>>>>>> ... I don't want to have to

>>>>>> write my composition function over again _in its entirety_

>>>>>> for Int, Float, Double, Long, whatever

>>>>>>

>> No, I'm not moving the target; you're losing the context.

>>

>

> No, I addressed your point above. What you say below

> is something separate.

>

>

>

>> I had a counterexample that went something like

>>

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

>> (a:A) => {

>> val b = f(a)

>> g(

>> b match {

>> case x:Int => -x

>> case x:Long => -x

>> case x:Float => -x

>> case x:Double => -x

>> case y => y

>> }

>> )

>> }

>> }

>>

>

> I don't think that's consistent with the universal quantification over

> the type parameters A, B and C? It seems to me you've really conflated

> 5 different functions, four of them with four particular instantiations

> of the type parameter B and one universal in all three type parameters.

>

> One of those four functions is this:

>

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

> x: A => g(-f(x))

> }

>

> There are four other for Long, Float and Double and the generic one I

> gave. The manipulation of the intermediate value is possible because

> the type has been nailed down.

>

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

>

>

>

>> ...

>>

>> --Rex

>>

>

>

> Randall Schulz

>

>

Fri, 2009-11-13, 07:47

#79
Re: Scaladoc that is actually useful?

On Thursday November 12 2009, Rex Kerr wrote:

> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:

> > You're moving the target. I addressed your statement above (copied

> >

> > here):

> > > > > ... I don't want to have to

> > > > > write my composition function over again _in its entirety_

> > > > > for Int, Float, Double, Long, whatever

>

> No, I'm not moving the target; you're losing the context.

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

is something separate.

> I had a counterexample that went something like

>

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

> (a:A) => {

> val b = f(a)

> g(

> b match {

> case x:Int => -x

> case x:Long => -x

> case x:Float => -x

> case x:Double => -x

> case y => y

> }

> )

> }

> }

I don't think that's consistent with the universal quantification over

the type parameters A, B and C? It seems to me you've really conflated

5 different functions, four of them with four particular instantiations

of the type parameter B and one universal in all three type parameters.

One of those four functions is this:

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

x: A => g(-f(x))

}

There are four other for Long, Float and Double and the generic one I

gave. The manipulation of the intermediate value is possible because

the type has been nailed down.

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

> ...

>

> --Rex

Randall Schulz

Fri, 2009-11-13, 07:57

#80
Re: Scaladoc that is actually useful?

When I first consulted the 2.8 docs I didn't like it, I thought there was a bug.

I got used to it, and now actually prefer it, the boxes (tables) for "methode inherited from"

actually give a more "zoomed out" overall view of what's

available, it's more dense, more info per square centimeter.

But if there's a way to get the best of both worlds, like a

button that woould toggle between an expanded and compressed view

it would certainly be ideal.

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

Max

On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

Earlier today I agreed with the original poster that there is a

problem with Scaladoc, in that it makes seemingly simple tasks

excessively complex for the programmer who has to get work done. That

discussion went off on some odd tangent about type systems that I will

ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer

in 2.8. The scaladoc sends me to

ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

SeqLike

PartialFunction

Function1

iterableLike

GenericTraversableTemplate

TraversableLike

AnyRef

Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

But then the Scaladoc could have a friendlier way of helping the new

user, such as inline expanding the docs for the traits, or at least,

copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother

knows more type theory than your mother".

Fri, 2009-11-13, 08:47

#81
Re: Scaladoc that is actually useful?

"So I submit that whatever it is that Tony defined is not actually

just a function but is something more strict (perhaps a "pure

function", a subset of the set of all valid functions from the

described input set to the described output set)."

I'm not sure why you would choose to use a non-mathematical definition

of function. The definitions in programming languages don't seem to

be a good base to go from:

C and Common Lisp call every procedure a function.

Pascal calls every procedure with a return value a function.

I'd call Scala's defs 'defs', or 'methods', and refrain from having a

function (instance of Function1 and friends) that is not referentially

transparent, as it's bloody confusing!

I agree with Tony that we should strive to make our types

self-documenting, but add that where they are not, *that* needs

documenting well.

As to the utility of scaladoc, it is awful so I tend to look at the

source instead. At least the source is more amusing.

2009/11/13 Rex Kerr :

> On Thu, Nov 12, 2009 at 7:25 PM, Randall R Schulz wrote:

>>

>> Functions are self-contained and pure. They know not of the world, other

>> than that portion of the world of mathematics that defines them.

>

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

> missing.

>

> In this case, yes, I agree, if functions that take 1-ary functions as

> arguments may only apply operations that are valid on the set of all 1-ary

> functions (and that operation happens to be composition, and you may not

> inspect the arguments or outputs to see if they themselves happen to be in

> the set of all 1-ary functions so you can't do anything there either), there

> is only one possible thing to do: compose the functions.

>

> I suppose that this type of property has nice consequences for provability

> of correctness of programs under some limited situations.

>

> It seems highly impractical, however, from a code duplication standpoint to

> never allow a generic function to understand something about the types that

> are thrown at it. So, yes, nice elegance, yay, but if I am going to program

> something, I don't want to have to write my composition function over again

> _in its entirety_ for Int, Float, Double, Long, whatever, just so that I

> keep the type signature conforming to the "functions only import the

> mathematics of their arguments" rule.

>

>>

>> Programmers have repeatedly been guilty of butchering established

>> concepts and terminology. Calling something a function that does not

>> conform to the definition of function universally agreed upon by

>> mathematicians is inexcusable.

>

> This is absolutely not the definition of function "universally agreed upon

> by mathematicians".

>

> For example,

>

> f(x) : R -> R = {

> x == 0 : 0

> x in Z : 1/x

> else: x

> }

>

> is a perfectly well-defined function on the reals, and it knows all about

> integers which is disallowed by the "pure" function definition above.

>

> The universal definition of function is, in mathematics, something very much

> like this:

>

> A (single-valued) _function_ from set A to set B is a rule that specifies

> for any element a in A an element b in B; we call this element in B f(a).

>

> It says nothing about how it does this. It says nothing about whether it

> knows about real numbers even though its arguments are perhaps functions.

> It just says it maps anything in the input set to some element of the output

> set.

>

> The mathematical definition does not admit side-effects, as it is simply a

> mapping. But it does not forbid _any_ method of transforming input to

> output.

>

> So I submit that whatever it is that Tony defined is not actually just a

> function but is something more strict (perhaps a "pure function", a subset

> of the set of all valid functions from the described input set to the

> described output set). I agree that a "function" that has side-effects is

> not a function in the mathematical sense, except inasmuch as it takes the

> world as an implicit argument and gives it as an implicit return value.

>

> --Rex

>

>

Fri, 2009-11-13, 13:37

#82
Re: Scaladoc that is actually useful?

I agree 100%!

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

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

- Josh

On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

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

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

- Josh

On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

Earlier today I agreed with the original poster that there is a

problem with Scaladoc, in that it makes seemingly simple tasks

excessively complex for the programmer who has to get work done. That

discussion went off on some odd tangent about type systems that I will

ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer

in 2.8. The scaladoc sends me to

ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

SeqLike

PartialFunction

Function1

iterableLike

GenericTraversableTemplate

TraversableLike

AnyRef

Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

But then the Scaladoc could have a friendlier way of helping the new

user, such as inline expanding the docs for the traits, or at least,

copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother

knows more type theory than your mother".

Fri, 2009-11-13, 14:57

#83
Re: Scaladoc that is actually useful?

It seems I only reply to you on this thread. :-)
Ok, without dismissing the problems with Scala API docs, which I do think it is an important topic, I think the problem here is not quite what you perceive it to be.
Java has relatively small (poor) interfaces, because the language makes it hard to have rich interfaces. Scala, on the other hand, enables very rich interfaces with a low implementation cost.
So, I ask you to consider this... how would you feel if all the methods for all these traits were simply listed one after the other, with their type signatures and descriptions? I don't know about you, but I'd feel tired just by looking at it, before even trying to read it.
When the class makes such extensive use of traits, however, I make use of previous knowledge. It won't help absolute beginners at first, but, at least, you get to reuse the knowledge you have previously acquired.
For instance, I have a fair knowledge of what I can do with an Iterable, so, knowing this class is IterableLike and TraversableLike already tells me a lot of things, without having to look up anything else. The same goes for PartialFunction and Function1.
And that means that, very much contrary to what you have stated, I *only* have to concentrate on:
ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

This is a huge decrease in the number of methods I have to look up. Furthermore, I know a lot of methods I'm used to are present as well. The alternative, of course, is not having most of these methods and having to reinvent the wheel each time I need something like them.

On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

--

Daniel C. Sobral

Veni, vidi, veterni.

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

This is a huge decrease in the number of methods I have to look up. Furthermore, I know a lot of methods I'm used to are present as well. The alternative, of course, is not having most of these methods and having to reinvent the wheel each time I need something like them.

On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

problem with Scaladoc, in that it makes seemingly simple tasks

excessively complex for the programmer who has to get work done. That

discussion went off on some odd tangent about type systems that I will

ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer

in 2.8. The scaladoc sends me to

ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

SeqLike

PartialFunction

Function1

iterableLike

GenericTraversableTemplate

TraversableLike

AnyRef

Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

But then the Scaladoc could have a friendlier way of helping the new

user, such as inline expanding the docs for the traits, or at least,

copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother

knows more type theory than your mother".

--

Daniel C. Sobral

Veni, vidi, veterni.

Fri, 2009-11-13, 15:07

#84
Re: Scaladoc that is actually useful?

2009/11/13 Tony Morris :

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

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

So that was the implicit assumption all along. I hope this helps

ending this rather fruitless discussion.

As I said yesterday too, Tony is not really talking about scala, as

you can see above, about the "unfortunate part of the Java legacy". He

talks about an abstraction that he wishes is equivalent to scala. Only

through those glasses/assumptions some docs seem redundant. Yet, Tony

is somehow against documenting assumptions, which is basically a

wishful thinking that the whole scala community will just adopt the

same set of assumptions as he, so he does not need to mention them.

_In scala_, which is the context of discussion, there is a type

hierarchy rooted at Any. For all A, A<:Any. Now, Any is proven to have

a whole range of methods applicable to it, like like hashCode(), like

toString(). So, for all A, one can safely call toString(). I'm sure

someone might scream "subverting!" or "lying!" or "goosfraba!" again

and again but that is completely irrelevant. Point is: in scala, a

signature, even as generic as the aptly named "boo" signature, has

*infinite* different implementations. Knock knock, this is the real

world hitting the door. Now, we can all pretend instead that the real

world is irrelevant, and we could rather reason only through our neat

abstractions, but as someone said, this is kind of Platonic. But

again, Plato was Plato for all his life, wasn't he?

Dimitris

> There is only *one possible answer*.

>

> Rex Kerr wrote:

>> On Thu, Nov 12, 2009 at 3:55 PM, Tony Morris > > wrote:

>>

>> e.g. What would you (could you possibly) write for this function?

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

>>

>>

>> That one? I don't know--it's titled "boo", so it should be a

>> surprise. Maybe it returns a function that prints out "Boo!" and

>> returns null. Maybe it returns the BooException and never completes

>> normally.

>>

>> How about this one?

>>

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

>>

>> Same type signature. Maybe it, I don't know, creates a function that

>> prints out the intermediate result of type B in addition to doing the

>> function composition?

>>

>> How about

>>

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

>>

>> Same type signature again. This might possibly catch if inputs are

>> null and throw null outputs rather than throwing exceptions, in

>> addition to composing the functions.

>>

>> If you don't document your functions, how are people supposed to know

>> whether and what side effects there are, and whether the function is

>> value-added (as in nullCatch) or not (as in the straightforward

>> function-composition boo that I assume you were imagining)?

>>

>> --Rex

>>

>

> --

> Tony Morris

> http://tmorris.net/

>

>

>

Fri, 2009-11-13, 15:07

#85
Re: Scaladoc that is actually useful?

Note though that DSLy things are not bad just in scaladocs - in

javadocs they are a nightmare too.

For example, here is a basic acknowledgement of the fact, in google

guice javadocs:

http://google-guice.googlecode.com/svn/trunk/javadoc/com/google/inject/B...

"Guice uses an embedded domain-specific language, or EDSL, to help you

create bindings simply and readably. This approach is great for

overall usability, but it does come with a small cost: it is difficult

to learn how to use the Binding EDSL by reading method-level javadocs.

"

I think we do need better ways. The various combinations that small

functions can create to yield interesting behavior is lost by just

looking only one by one, in some order, the function definitions

themselves. A graph notation of an api should be promising, but how

would one create an understandable graph of higher-order functions? A

good answer to the latter would immediately open the prospect of a

very interesting project.

Dimitris

2009/11/13 Josh Suereth :

> I agree 100%!

>

> I also think when you start placing implicits into the mix, you need new

> ways of documenting things. Example usage becomes *very* important,

> especially when every example would show: import foo.myawesomedsl._ or

> class SomeClass extends MyAwesomeDSLTrait

>

> When I first went to learn a few of these DSL-y libraries via scaladoc, it

> becomes interesting trying to hold all the classes in your head while you

> drill around looking for methods and types that do nothing but provide handy

> operators.

>

> - Josh

>

> On Thu, Nov 12, 2009 at 11:36 PM, Cay Horstmann

> wrote:

>>

>> Earlier today I agreed with the original poster that there is a

>> problem with Scaladoc, in that it makes seemingly simple tasks

>> excessively complex for the programmer who has to get work done. That

>> discussion went off on some odd tangent about type systems that I will

>> ignore.

>>

>> Back to the original complaint...suppose I want to use an ArrayBuffer

>> in 2.8. The scaladoc sends me to

>>

>> ResizableArray

>> Builder

>> IndexedSeqLike

>> IndexedSeqLike (again, but this time not mutable)

>> BufferLike

>> Shrinkable

>> Growable

>> SeqLike

>> PartialFunction

>> Function1

>> iterableLike

>> GenericTraversableTemplate

>> TraversableLike

>> AnyRef

>> Any

>>

>> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

>> But then the Scaladoc could have a friendlier way of helping the new

>> user, such as inline expanding the docs for the traits, or at least,

>> copying out the summary method statements.

>>

>> This really needs some fresh thinking without detours into "my mother

>> knows more type theory than your mother".

>

>

Fri, 2009-11-13, 15:17

#86
Re: Scaladoc that is actually useful?

It doesn't compile.
There are three ways you can go about it:
1. Compose f and g.
2. Do not return (throw an exception, for instance).
3. Return a function that does not return (null, for example).

On Fri, Nov 13, 2009 at 3:00 AM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:

--

Daniel C. Sobral

Veni, vidi, veterni.

On Fri, Nov 13, 2009 at 3:00 AM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:

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

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

here):

> > > ... I don't want to have to

> > > write my composition function over again _in its entirety_ for

> > > Int, Float, Double, Long, whatever

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

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

(a:A) => {

val b = f(a)

g(

b match {

case x:Int => -x

case x:Long => -x

case x:Float => -x

case x:Double => -x

case y => y

}

)

}

}

which absolutely obeys the types _viewed as sets_. I have constructed a function that, for each input in the set

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

produces an element in the set

(A=>C)

which is what is required of a mathematical function.

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

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

--Rex

--

Daniel C. Sobral

Veni, vidi, veterni.

Fri, 2009-11-13, 15:27

#87
Re: Scaladoc that is actually useful?

As a side note, I'd love if ScalaDoc provided a search function. I open up a class, type up a method name on the search field, and it either shows me the method definition (in another trait/class, if needed), or tells me it isn't defined for that class.

On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

--

Daniel C. Sobral

Veni, vidi, veterni.

On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann <cay [dot] horstmann [at] gmail [dot] com> wrote:

problem with Scaladoc, in that it makes seemingly simple tasks

excessively complex for the programmer who has to get work done. That

discussion went off on some odd tangent about type systems that I will

ignore.

Back to the original complaint...suppose I want to use an ArrayBuffer

in 2.8. The scaladoc sends me to

ResizableArray

Builder

IndexedSeqLike

IndexedSeqLike (again, but this time not mutable)

BufferLike

Shrinkable

Growable

SeqLike

PartialFunction

Function1

iterableLike

GenericTraversableTemplate

TraversableLike

AnyRef

Any

Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

But then the Scaladoc could have a friendlier way of helping the new

user, such as inline expanding the docs for the traits, or at least,

copying out the summary method statements.

This really needs some fresh thinking without detours into "my mother

knows more type theory than your mother".

--

Daniel C. Sobral

Veni, vidi, veterni.

Fri, 2009-11-13, 15:27

#88
RE: Scaladoc that is actually useful?

Note that things like the scaladoc for things like the forall function is

/** Return true iff the given predicate `p` yields true for all elements

* of this traversable.

*

* @note May not terminate for infinite-sized collections.

* @param p the predicate

*/

Speaking from the perspective of someone who has been bitten

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

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

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

***ambiguous***:/** Return true iff the given predicate `p` yields true for all elements

* of this traversable.

*

* @note May not terminate for infinite-sized collections.

* @param p the predicate

*/

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

Speaking from the perspective of someone who has been bitten

***in the real world***by ambiguous or incomplete documentation (String.substring anyone?), extensive documentation of both what the function does*and how it does it*(or what it may leave undefined) is critical in the long run, although it's understandable that it is something left to last (it's neither a glamorous or interesting thing to do).I'll say it again: comprehensive documentation creates wider adoption - it's as simple as that.

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

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

Fri, 2009-11-13, 15:37

#89
Re: Scaladoc that is actually useful?

Whilst discussing Scaladoc...

What I'd love is a way too see what methods are in scope via

self-typing, and where they originate.

On Fri, Nov 13, 2009 at 2:04 PM, Daniel Sobral wrote:

> As a side note, I'd love if ScalaDoc provided a search function. I open up a

> class, type up a method name on the search field, and it either shows me the

> method definition (in another trait/class, if needed), or tells me it isn't

> defined for that class.

>

> On Fri, Nov 13, 2009 at 2:36 AM, Cay Horstmann

> wrote:

>>

>> Earlier today I agreed with the original poster that there is a

>> problem with Scaladoc, in that it makes seemingly simple tasks

>> excessively complex for the programmer who has to get work done. That

>> discussion went off on some odd tangent about type systems that I will

>> ignore.

>>

>> Back to the original complaint...suppose I want to use an ArrayBuffer

>> in 2.8. The scaladoc sends me to

>>

>> ResizableArray

>> Builder

>> IndexedSeqLike

>> IndexedSeqLike (again, but this time not mutable)

>> BufferLike

>> Shrinkable

>> Growable

>> SeqLike

>> PartialFunction

>> Function1

>> iterableLike

>> GenericTraversableTemplate

>> TraversableLike

>> AnyRef

>> Any

>>

>> Ok, maybe it's the Scala way to pick up lots of fragmentary traits.

>> But then the Scaladoc could have a friendlier way of helping the new

>> user, such as inline expanding the docs for the traits, or at least,

>> copying out the summary method statements.

>>

>> This really needs some fresh thinking without detours into "my mother

>> knows more type theory than your mother".

>

>

>

> --

> Daniel C. Sobral

>

> Veni, vidi, veterni.

>

Fri, 2009-11-13, 15:37

#90
Re: Scaladoc that is actually useful?

I just can't believe a simple question on this list turned into a 40-deep discussion about type theory and functional programming. What newcomer would be put off by that? :)

Dave

---

My Blog: http://www.naildrivin5.com/blog

Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour

Fork me on Github: http://davetron5000.github.com

On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

Dave

---

My Blog: http://www.naildrivin5.com/blog

Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour

Fork me on Github: http://davetron5000.github.com

On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

On Thursday November 12 2009, Rex Kerr wrote:

> On Thu, Nov 12, 2009 at 11:46 PM, Randall R Schulz wrote:

> > You're moving the target. I addressed your statement above (copied

> >

> > here):

> > > > > ... I don't want to have to

> > > > > write my composition function over again _in its entirety_

> > > > > for Int, Float, Double, Long, whatever

>

> No, I'm not moving the target; you're losing the context.

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

is something separate.

> I had a counterexample that went something like

>

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

> (a:A) => {

> val b = f(a)

> g(

> b match {

> case x:Int => -x

> case x:Long => -x

> case x:Float => -x

> case x:Double => -x

> case y => y

> }

> )

> }

> }

I don't think that's consistent with the universal quantification over

the type parameters A, B and C? It seems to me you've really conflated

5 different functions, four of them with four particular instantiations

of the type parameter B and one universal in all three type parameters.

One of those four functions is this:

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

x: A => g(-f(x))

}

There are four other for Long, Float and Double and the generic one I

gave. The manipulation of the intermediate value is possible because

the type has been nailed down.

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

> ...

>

> --Rex

Randall Schulz

Fri, 2009-11-13, 15:37

#91
Re: Scaladoc that is actually useful?

I second this. Or p(x) => x + 1 it.

I think to assist in this we need:

- the concept of a doclet (this solves the "show all methods vs. traits" debate, as well as many, many others)

- an easy to follow means of submitting patches to the docs

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

Dave

---

My Blog: http://www.naildrivin5.com/blog

Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour

Fork me on Github: http://davetron5000.github.com

On Fri, Nov 13, 2009 at 9:19 AM, christopher marshall <oxbow_lakes [at] hotmail [dot] com> wrote:

I think to assist in this we need:

- the concept of a doclet (this solves the "show all methods vs. traits" debate, as well as many, many others)

- an easy to follow means of submitting patches to the docs

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

Dave

---

My Blog: http://www.naildrivin5.com/blog

Scala Tour for Java Developers: http://www.naildrivin5.com/scalatour

Fork me on Github: http://davetron5000.github.com

On Fri, Nov 13, 2009 at 9:19 AM, christopher marshall <oxbow_lakes [at] hotmail [dot] com> wrote:

Note that things like the scaladoc for things like the forall function is*ambiguous*:

/** Return true iff the given predicate `p` yields true for all elements

* of this traversable.

*

* @note May not terminate for infinite-sized collections.

* @param p the predicate

*/

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

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

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

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

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

Fri, 2009-11-13, 15:47

#92
Re: Scaladoc that is actually useful?

On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

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

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

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

--Rex

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

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

What you say below is something separate.

> I had a counterexample that went something like

>

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

> (a:A) => {

> val b = f(a)

> g(

> b match {

> case x:Int => -x

> case x:Long => -x

> case x:Float => -x

> case x:Double => -x

> case y => y

> }

> )

> }

> }

I don't think that's consistent with the universal quantification over

the type parameters A, B and C? It seems to me you've really conflated

5 different functions, four of them with four particular instantiations

of the type parameter B and one universal in all three type parameters.

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

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

One of those four functions is this:

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

x: A => g(-f(x))

}

There are four other for Long, Float and Double and the generic one I

gave. The manipulation of the intermediate value is possible because

the type has been nailed down.

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

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

--Rex

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

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

Fri, 2009-11-13, 15:57

#93
Re: Scaladoc that is actually useful?

Scala recommends not using isInstanceOf/asInstanceOf, because you may accidentally lie about types when you use them.
Which proves the point.

On Fri, Nov 13, 2009 at 12:17 PM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:

--

Daniel C. Sobral

Veni, vidi, veterni.

On Fri, Nov 13, 2009 at 12:17 PM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:

On Fri, Nov 13, 2009 at 1:29 AM, Randall R Schulz <rschulz [at] sonic [dot] net> wrote:

What you say below is something separate.

> I had a counterexample that went something like

>

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

> (a:A) => {

> val b = f(a)

> g(

> b match {

> case x:Int => -x

> case x:Long => -x

> case x:Float => -x

> case x:Double => -x

> case y => y

> }

> )

> }

> }

I don't think that's consistent with the universal quantification over

the type parameters A, B and C? It seems to me you've really conflated

5 different functions, four of them with four particular instantiations

of the type parameter B and one universal in all three type parameters.

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

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

One of those four functions is this:

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

x: A => g(-f(x))

}

There are four other for Long, Float and Double and the generic one I

gave. The manipulation of the intermediate value is possible because

the type has been nailed down.

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

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

--Rex

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

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

--

Daniel C. Sobral

Veni, vidi, veterni.

Fri, 2009-11-13, 16:07

#94
Re: Scaladoc that is actually useful?

On Friday November 13 2009, christopher marshall wrote:

> Note that things like the scaladoc for things like the forall

> function is *ambiguous*:

>

> /** Return true iff the given predicate `p` yields true for all

> elements * of this traversable.

> *

> * @note May not terminate for infinite-sized collections.

> * @param p the predicate

> */

>

> Does this return true for an empty collection? (I don't think the

> "average" developer is likely to definitively know the answer to this

> as it's a subtle point of logic.)

It can be rephrased to remove the ambiguity:

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

returns false."

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

returns true."

> ...

>

> Speaking from the perspective of someone who has been bitten *in the

> real world* by ambiguous or incomplete documentation

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

And we've all had this experience.

> ...

Randall Schulz

Fri, 2009-11-13, 16:17

#95
RE: Scaladoc that is actually useful?

> It can be rephrased to remove the ambiguity:

>

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

> returns false."

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

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

>

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

> returns false."

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

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

Fri, 2009-11-13, 16:17

#96
Re: Scaladoc that is actually useful?

On Fri, Nov 13, 2009 at 3:04 PM, Daniel Sobral wrote:

> As a side note, I'd love if ScalaDoc provided a search function. I open up a

> class, type up a method name on the search field, and it either shows me the

> method definition (in another trait/class, if needed), or tells me it isn't

> defined for that class.

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

Fri, 2009-11-13, 16:27

#97
Re: Scaladoc that is actually useful?

On Friday November 13 2009, christopher marshall wrote:

> > It can be rephrased to remove the ambiguity:

> >

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

> > returns false."

>

> This is still ambiguous as you've used if instead of iff (which,

> again, the "average" developer may not be familiar with)! And you

> still haven't told me whether the implementation will continue to

> evaluate the predicate after the result of the function is

> effectively decided (although the original doc about infinite

> collections gives a hint as to whether this is the case).

I didn't intend to rewrite the documentation, just show how that one

ambiguity might be expunged.

Randall Schulz

Fri, 2009-11-13, 16:27

#98
Re: Scaladoc that is actually useful?

On Fri, Nov 13, 2009 at 9:33 AM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:

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

If you use them to make a whenInstanceOf construct:

def whenInstanceOf[A,B,C](a:A)(f:B=>C):Option[C] = {

if (a.isInstanceOf[B]) Some(f(a.asInstanceOf[B]))

else None

}

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

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

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

--Rex

Scala recommends not using isInstanceOf/asInstanceOf, because you may accidentally lie about types when you use them. Which proves the point.

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

If you use them to make a whenInstanceOf construct:

def whenInstanceOf[A,B,C](a:A)(f:B=>C):Option[C] = {

if (a.isInstanceOf[B]) Some(f(a.asInstanceOf[B]))

else None

}

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

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

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

--Rex

Fri, 2009-11-13, 16:37

#99
Re: Scaladoc that is actually useful?

All,

Without becoming to philosophical, I'd like to add a few thoughts to this

'academically challenging' (e.g. type theory) versus

'industrially acceptable' (e.g. Java) discusson.

Ignore if not interested.

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

- its complexity (I use complex as opposed to simple)

- its difficulty (I use difficult as oppopsed to easy)

Complexity can be reduced using abstraction

(here I use abstraction the software way: as a synonym of symplicifcation).

We should value abstraction because of this!

In my opinion there is no risk associated with this kind of abstraction:

the simpler it gets, the better.

Difficulty can only be demistified, I'm afraid,

and some brains may never understand something that has a certain difficulty.

In general, there is no relationship between complexity and difficulty,

but, something can be so complex that it may seem to be difficult

(our brains can only cope with a limited amount of complexity).

There is also specific versus generic. All to often similar specific code

fragments and similar specific code templates are written.

Reusability can be increased by using abstraction

(here I use abstraction the mathematics way: as a synonym of generalization).

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

But, in my opinion there is a risk associated with this kind of abstraction.

First it may increase complexity (Function[-X, +Y] is more complex than Function),

second, and more important, it may increase difficulty (at least for some brains).

So, yes, abstract (in the sense of generic) code should be well documented.

Of course, type information is a very important documentation of it,

but, in my opinion, providing many examples (also in the API documentation!) of

how to use specific instances of it is way more important in order to demistify it.

Some brains tend to learn by specific examples.

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

Luc

--

__~O

-\ <,

(*)/ (*)

reality goes far beyond imagination

Without becoming to philosophical, I'd like to add a few thoughts to this

'academically challenging' (e.g. type theory) versus

'industrially acceptable' (e.g. Java) discusson.

Ignore if not interested.

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

- its complexity (I use complex as opposed to simple)

- its difficulty (I use difficult as oppopsed to easy)

Complexity can be reduced using abstraction

(here I use abstraction the software way: as a synonym of symplicifcation).

We should value abstraction because of this!

In my opinion there is no risk associated with this kind of abstraction:

the simpler it gets, the better.

Difficulty can only be demistified, I'm afraid,

and some brains may never understand something that has a certain difficulty.

In general, there is no relationship between complexity and difficulty,

but, something can be so complex that it may seem to be difficult

(our brains can only cope with a limited amount of complexity).

There is also specific versus generic. All to often similar specific code

fragments and similar specific code templates are written.

Reusability can be increased by using abstraction

(here I use abstraction the mathematics way: as a synonym of generalization).

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

But, in my opinion there is a risk associated with this kind of abstraction.

First it may increase complexity (Function[-X, +Y] is more complex than Function),

second, and more important, it may increase difficulty (at least for some brains).

So, yes, abstract (in the sense of generic) code should be well documented.

Of course, type information is a very important documentation of it,

but, in my opinion, providing many examples (also in the API documentation!) of

how to use specific instances of it is way more important in order to demistify it.

Some brains tend to learn by specific examples.

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

Luc

--

__~O

-\ <,

(*)/ (*)

reality goes far beyond imagination

Fri, 2009-11-13, 16:47

#555
Re: Scaladoc that is actually useful?

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

"There are very few problems in programming that can't be solved by

adding another level of indirection. Except, perhaps, for too much

indirection..."

On Fri, Nov 13, 2009 at 3:35 PM, Luc Duponcheel

wrote:

> All,

>

> Without becoming to philosophical, I'd like to add a few thoughts to this

> 'academically challenging' (e.g. type theory) versus

> 'industrially acceptable' (e.g. Java) discusson.

>

> Ignore if not interested.

>

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

>

> - its complexity (I use complex as opposed to simple)

> - its difficulty (I use difficult as oppopsed to easy)

>

> Complexity can be reduced using abstraction

> (here I use abstraction the software way: as a synonym of symplicifcation).

>

> We should value abstraction because of this!

>

> In my opinion there is no risk associated with this kind of abstraction:

> the simpler it gets, the better.

>

> Difficulty can only be demistified, I'm afraid,

> and some brains may never understand something that has a certain

> difficulty.

>

> In general, there is no relationship between complexity and difficulty,

> but, something can be so complex that it may seem to be difficult

> (our brains can only cope with a limited amount of complexity).

>

> There is also specific versus generic. All to often similar specific code

> fragments and similar specific code templates are written.

>

> Reusability can be increased by using abstraction

> (here I use abstraction the mathematics way: as a synonym of

> generalization).

>

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

>

> But, in my opinion there is a risk associated with this kind of abstraction.

> First it may increase complexity (Function[-X, +Y] is more complex than

> Function),

> second, and more important, it may increase difficulty (at least for some

> brains).

>

> So, yes, abstract (in the sense of generic) code should be well documented.

> Of course, type information is a very important documentation of it,

> but, in my opinion, providing many examples (also in the API documentation!)

> of

> how to use specific instances of it is way more important in order to

> demistify it.

>

> Some brains tend to learn by specific examples.

> Other brains (including my brain) tend to learn by generalization.

>

> Luc

>

> --

> __~O

> -\ <,

> (*)/ (*)

>

> reality goes far beyond imagination

>

>

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/

>

>

>