- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers
Re: Scaladoc that is actually useful?
Are you sure they're not listed?
In Scala at least the primary constructor is looked at as "the arguments to the class." So it would be listed with documentation of the class itself.
-------------------------------------
Donald McLean wrote:
(observations based on 2.7.7 - feel free to say that something will be
better in 2.8 but only if it actually is)
I'm new to Scala but have been using Java for more than 10 years now.
One of the stumbling blocks that I am running into learning the
language is that the Scaladoc for many of the library classes is
nearly useless. The mutable LinkedList, for example is almost
impossible for a newbie to use because it is so completely unlike most
Java collections and the constructor is not listed in the Scaladoc.
So why aren't constructors listed in the Scaladoc? (though I haven't
yet progressed to the point where the syntax for the LinkedList class
makes sense yet, even if I have figured out how to use it)
And maybe some actual, even useful, descriptive text? If the answer is
"well, nobody has gotten around to it yet," I can understand that (and
will probably volunteer to help correct the problem, just as soon as I
can understand it myself)
Re: Scaladoc that is actually useful?
On Thursday November 12 2009, Dimitris Andreou wrote:
> 2009/11/13 Tony Morris :
> > Rex,
> > I can read your code just fine. I assure you, the signature given
> > is once-inhabited. There is even a proof of this fact. It's a well
> > understood basic fact of computational theory.
>
> The problem is that a signature never captures the implicit "world"
> argument that all functions have (otherwise, please show me your
> functions having the "world" argument from which you access all of
> scala libraries) . So the signature definitely has *not* just one
> instance, but infinitely many.
Functions are self-contained and pure. They know not of the world, other
than that portion of the world of mathematics that defines them.
A subroutine / method that accesses values not passed to it as arguments
does not compute a function. A method that produces different values
when called repeatedly with the same arguments does not compute a
function.
Not all methods compute functions. And not all signatures are "singly
occupied," and such signatures clearly demand further characterization.
> If you don't assume that a function is able to compute other
> functions, just because it didn't have them as arguments, you talk
> about something else but definitely not about scala programming. May
> I remind that the discussion is about _scala_ docs.
It is true Scala programs can readily transgress functional strictures,
but when you say this:
def func[A, B, C](f: A => B, g: B => C): A => C
you've said enough.
It is perfectly correct that to say more (in natural language) is either
redundant or erroneous. Of course, while redundancy isn't a cardinal
sin, erroneousness is.
So tread carefully. Natural language, including "meaningful names" has
equal power to mislead as to enlighten. Formal language is either
understood or not understood. It cannot lie or mislead through
unintended connotations.
> This point has already been made by Rex but lets try it again :)
Programmers have repeatedly been guilty of butchering established
concepts and terminology. Calling something a function that does not
conform to the definition of function universally agreed upon by
mathematicians is inexcusable.
> Regards,
> Dimitris
Randall Schulz
Re: Scaladoc that is actually useful?
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
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
>
>
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
Re: Scaladoc that is actually useful?
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
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
>
>
Re: Scaladoc that is actually useful?
Please don't be dishonest. This is the *fourth time*.
Let's restate the assumptions:
* Assume termination
* No subverting the types
Dimitris Andreou wrote:
> 2009/11/13 Tony Morris :
>
>> Actually, I didn't claim that at all.
>>
>
> Erm... "I assure you, the signature given is once-inhabited" - and you
> kind of insisted that you were talking about scala...
>
>
>> For the fourth time...
>>
>> ah bugger it. And no, the halting problem does not contradict that at
>> all (ugh!).
>>
>
> But you are right about that, of course. It doesn't take a halting
> problem to prove that there are non-terminating implementations (which
> simultaneously conform to the supposedly once-habitated signature
> though!), one can just create a trivial example.
>
> Bye!
>
>> Dimitris Andreou wrote:
>>
>>> Since *you* claimed that there was only a single implementation of
>>> that signature, it is *you* that imply that all possible
>>> implementations are halting. Guess what, that's exactly what the
>>> halting problem contradicts :)
>>>
>>> See you! It was fun :)
>>> I really like you you know, but sometimes I think you just rant
>>> unchecked (with no suppress compiler option :) )
>>>
>>> Good night all,
>>> Dimitris
>>>
>>> 2009/11/13 Tony Morris :
>>>
>>>
>>>> "I am not discussing this matter any further until you have solved the
>>>> turing halting problem!"
>>>>
>>>> That's fine by me, I'm exhausted :) Seeya!
>>>>
>>>> Dimitris Andreou wrote:
>>>>
>>>>
>>>>> Omg, you used...english! Please encode these constrains as a scala
>>>>> signature and I go home. :)
>>>>>
>>>>> 2009/11/13 Tony Morris :
>>>>>
>>>>>
>>>>>
>>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>>> a third time:
>>>>>>
>>>>>> * No subverting the types
>>>>>> * Assume termination
>>>>>>
>>>>>> *crosses fingers*
>>>>>>
>>>>>> Dimitris Andreou wrote:
>>>>>>
>>>>>>
>>>>>>
>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>>> see that.
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>>
>>>>>>> This is the signature I see you gave:
>>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>>
>>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>>> signature I missed, please repeat.
>>>>>>>
>>>>>>> Dimitris
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>>
>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>>> not even a debate.
>>>>>>>>>>
>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>>
>>>>>>>>>> I will repeat myself:
>>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>>
>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>>
>>>>>>>>>> I am exhausted, you win.
>>>>>>>>>>
>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> Rex,
>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>>
>>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>>
>>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>>
>>>>>>>>>>> Regards,
>>>>>>>>>>> Dimitris
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>>
>>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>>> P Q P->Q
>>>>>>>>>>>> 0 0 1
>>>>>>>>>>>> 0 1 1
>>>>>>>>>>>> 1 0 0
>>>>>>>>>>>> 1 1 1
>>>>>>>>>>>>
>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>>
>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>>
>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>>
>>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> Tony,
>>>>>>>>>>>>>
>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>>
>>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>>
>>>>>>>>>>>>> --Rex
>>>>>>>>>>>>>
>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>> > wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>> just make
>>>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>> interesting one.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>>>>>> if foo
>>>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>> leaving
>>>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>> > might have practical utility.
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > For example,
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>>>>>> > val b = f(a)
>>>>>>>>>>>>> > g(
>>>>>>>>>>>>> > b match {
>>>>>>>>>>>>> > case x:Int : -x
>>>>>>>>>>>>> > case x:Long : -x
>>>>>>>>>>>>> > case x:Float : -x
>>>>>>>>>>>>> > case x:Double: -x
>>>>>>>>>>>>> > case y: y
>>>>>>>>>>>>> > }
>>>>>>>>>>>>> > )
>>>>>>>>>>>>> > }
>>>>>>>>>>>>> > }
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>> the idea.)
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>>>>>> what is
>>>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>> what is
>>>>>>>>>>>>> > promised.
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>> one-to-one
>>>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>> > system is impractical.)
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > --Rex
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>>
>>>>>>>>>>>>> > >> wrote:
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>> ability to
>>>>>>>>>>>>> > print
>>>>>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>> legacy.
>>>>>>>>>>>>> >
>>>>>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>>>>>> >
>>>>>>>>>>>>> >
>>>>>>>>>>>>>
>>>>>>>>>>>>> --
>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>> --
>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>> --
>>>>>>>>>> Tony Morris
>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>> --
>>>>>>>> Tony Morris
>>>>>>>> http://tmorris.net/
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>> --
>>>>>> Tony Morris
>>>>>> http://tmorris.net/
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>> --
>>>> Tony Morris
>>>> http://tmorris.net/
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> Tony Morris
>> http://tmorris.net/
>>
>>
>>
>>
>
>
Re: Scaladoc that is actually useful?
Alright, I think we can finally agree and end this peacefully. The
signature *plus* some assumptions (encoded in perfectly good english)
may make it once-habitated. The scala signature itself does _not_,
since it does not by itself provide any extra assumptions. Many of us
thought perhaps misunderstood that you were saying that the latter is
also once-habitated by itself, so no english were needed in the
scaladocs - while they *are* needed to make this extra claim, thus the
debate. End of story. Is that ok with you?
2009/11/13 Tony Morris :
> Please don't be dishonest. This is the *fourth time*.
>
> Let's restate the assumptions:
>
> * Assume termination
> * No subverting the types
>
> Dimitris Andreou wrote:
>> 2009/11/13 Tony Morris :
>>
>>> Actually, I didn't claim that at all.
>>>
>>
>> Erm... "I assure you, the signature given is once-inhabited" - and you
>> kind of insisted that you were talking about scala...
>>
>>
>>> For the fourth time...
>>>
>>> ah bugger it. And no, the halting problem does not contradict that at
>>> all (ugh!).
>>>
>>
>> But you are right about that, of course. It doesn't take a halting
>> problem to prove that there are non-terminating implementations (which
>> simultaneously conform to the supposedly once-habitated signature
>> though!), one can just create a trivial example.
>>
>> Bye!
>>
>>> Dimitris Andreou wrote:
>>>
>>>> Since *you* claimed that there was only a single implementation of
>>>> that signature, it is *you* that imply that all possible
>>>> implementations are halting. Guess what, that's exactly what the
>>>> halting problem contradicts :)
>>>>
>>>> See you! It was fun :)
>>>> I really like you you know, but sometimes I think you just rant
>>>> unchecked (with no suppress compiler option :) )
>>>>
>>>> Good night all,
>>>> Dimitris
>>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> "I am not discussing this matter any further until you have solved the
>>>>> turing halting problem!"
>>>>>
>>>>> That's fine by me, I'm exhausted :) Seeya!
>>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> Omg, you used...english! Please encode these constrains as a scala
>>>>>> signature and I go home. :)
>>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>>>> a third time:
>>>>>>>
>>>>>>> * No subverting the types
>>>>>>> * Assume termination
>>>>>>>
>>>>>>> *crosses fingers*
>>>>>>>
>>>>>>> Dimitris Andreou wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>>>> see that.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>>>
>>>>>>>> This is the signature I see you gave:
>>>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>>>
>>>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>>>> signature I missed, please repeat.
>>>>>>>>
>>>>>>>> Dimitris
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>>>
>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>>>> not even a debate.
>>>>>>>>>>>
>>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>>>
>>>>>>>>>>> I will repeat myself:
>>>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>>>
>>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>>>
>>>>>>>>>>> I am exhausted, you win.
>>>>>>>>>>>
>>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> Rex,
>>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>>>
>>>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>>>
>>>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>>>
>>>>>>>>>>>> Regards,
>>>>>>>>>>>> Dimitris
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>>>> P Q P->Q
>>>>>>>>>>>>> 0 0 1
>>>>>>>>>>>>> 0 1 1
>>>>>>>>>>>>> 1 0 0
>>>>>>>>>>>>> 1 1 1
>>>>>>>>>>>>>
>>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>>>
>>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>>>
>>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>>>
>>>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> Tony,
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> --Rex
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>>> > wrote:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>>> just make
>>>>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>>> interesting one.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>>>>>>> if foo
>>>>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>>> leaving
>>>>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>>> > might have practical utility.
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > For example,
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>>>>>>> > val b = f(a)
>>>>>>>>>>>>>> > g(
>>>>>>>>>>>>>> > b match {
>>>>>>>>>>>>>> > case x:Int : -x
>>>>>>>>>>>>>> > case x:Long : -x
>>>>>>>>>>>>>> > case x:Float : -x
>>>>>>>>>>>>>> > case x:Double: -x
>>>>>>>>>>>>>> > case y: y
>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>> > )
>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>>> the idea.)
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>>>>>>> what is
>>>>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>>> what is
>>>>>>>>>>>>>> > promised.
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>>> one-to-one
>>>>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>>> > system is impractical.)
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > --Rex
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> > >> wrote:
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>>> ability to
>>>>>>>>>>>>>> > print
>>>>>>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>>> legacy.
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> --
>>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>> --
>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>> --
>>>>>>>>>>> Tony Morris
>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 8:04 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
RE: Scaladoc that is actually useful?
Not to mention the silliness of the argument.
-------------------------------------
christopher marshall wrote:
This is what Tony said to the *first* person who said that he disagreed that Tony's boo function should be commented as it would not be clear to all (which he had written quite "passively"):
"I think you should seriously consider your position, since your apathy and indirect advocacy for poor education is part of the problem, not the solution"
I'm sorry, but I happen to find this sort of language and approach unwarranted, unnecessary and does not belong on a professional mailing list. It has all the hallmarks of a troll: i.e. it falls short of direct personal abuse but can largely be read/interpreted as such.
I think it was this initial attitude that largely set the combative and confrontational tone for the rest of the discussion.
Chris
Date: Sun, 15 Nov 2009 23:47:19 +0100
Subject: Re: [scala-user] Scaladoc that is actually useful?
From: viktor [dot] klang [at] gmail [dot] com
To: tonymorris [at] gmail [dot] com
CC: dave [dot] l [dot] griffith [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch
It a rare occurrence, but I have to say that I'm with Tony on this one.
One might not appreciate the tone of Tony in this series of e-mails, but he's kept it balanced throughout his correspondence.
On Sun, Nov 15, 2009 at 10:24 PM, Tony Morris wrote:
Sorry Dave and list, I meant to reply off list. If you could that I Dave
I'd appreciate it.
Tony Morris wrote:
> Your motives are exposed. There is no "internet victory." I stated my
> motives up front. I wish to educate. I succeeded. I have personal
> testimonies to that effect. I even have people that got off first base
> and explored interesting questions down the path! Yes this excites me,
> "internet victory" (whatever that means) doesn't. I'll hand that over to
> you for whatever purpose it serves.
>
> I'll read back through it some day, but it is rather uninteresting.
> Consider my possible motivations for reading myself repeating a well
> established fact, to appease what I can only consider is a lack of
> comprehension. There is nothing for me to gain here, neither to learn
> nor for teaching.
>
> You are right that the thread may have turned people off. I know 2
> people who have thought, to paraphrase, "how can programmers be that
> stupid!?" I discourage that type of discourse and I think it is unfair,
> but they think it nonetheless. I'm sure it affected their prejudices of
> using Scala. I also think it is unfair that while stating highly
> relevant, proven, educational facts may or may not be contrary to
> "appeasing the point of view of someone outside the community" (is it
> really?), then there should be any apprehension of doing exactly that.
>
> Do you find it offensive that there are people who learned by thinking
> about it?
>
> Dave Griffith wrote:
>
>> I thought about this for a bit, and honestly have neither the time nor the
>> energy to do so.
>> You can claim internet victory because of that if you wish, and I'd bet good
>> money that you will. Alternatively, you could read back through the rather
>> thuggishly hijacked thread and try
>> to imagine how you must sound to others. In particular, how you must sound
>> others
>> who don't share your priors about what the appropriate domain of
>> discourse of a Scala
>> mailing list should be. For extra points, imagine it from the point of
>> view of someone
>> outside the community, trying to decide whether to use Scala or not. How
>> effective do you
>> really think you've been at "educating" them?
>>
>> --Dave Griffith
>>
>>
>>
>>
>
>
--
Tony Morris
http://tmorris.net/
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/
>
>
>
Re: Scaladoc that is actually useful?
You point is well taken which is why i also included convolution as another example.
Best wishes,
--greg
On Mon, Nov 16, 2009 at 9:21 AM, Johannes Rudolph <johannes [dot] rudolph [at] googlemail [dot] com> wrote:
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117
+1 206.650.3740
http://biosimilarity.blogspot.com
Re: Scaladoc that is actually useful?
I didn't say that the type signature was all that you needed. I gave a
specific case. It is a fact that, were it not also lamentable, would
also be somewhat amusing that this is causing a "debate."
If you wish to understand why => means implication and why Either means
disjunction and why Tuple2 means conjunction and ..., then I direct you
to any introduction to the Curry-Howard isomorphism, also known as (wait
for it!), Types as Theorems.
There is also a great paper out there on what is commonly called Free
Theorems.
I am too exhausted to pursue this matter. I was hoping for a different
outcome. Hopefully the silent audience did some thinking!
christopher marshall wrote:
> How does a function:
>
> def foo(i: Int) : String
>
> Tell me anything about what the function *actually does*, regardless
> of whether, under some given definition of "implies" the statement Int
> => String is "true", given foo. I must be completely missing some
> point here because for the life of me I don't really understand the
> train of thought that says that the type signature of a function is
> all you need to parse to understand what the function does.
>
> > Date: Fri, 13 Nov 2009 10:31:34 +1000
> > From: tonymorris [at] gmail [dot] com
> > To: oxbow_lakes [at] hotmail [dot] com
> > CC: jim [dot] andreou [at] gmail [dot] com; ichoran [at] gmail [dot] com; scala-user [at] listes [dot] epfl [dot] ch
> > Subject: Re: [scala-user] Scaladoc that is actually useful?
> >
> >
> >
> > christopher marshall wrote:
> > > The fact that you are using => to mean the mathematical/logic
> > > "implies" seems to ignore the fact that in Scala, => means no such
> > > thing. A, B and C are not statements/sentences: in a scala signature,
> > > they are types and the signature tells me nothing about what the
> > > method/function actually does! *Why are we even arguing about this?*
> >
> > Actually, in Scala it means exactly that. Please see the C-H
> Isomorphism.
> >
> > --
> > Tony Morris
> > http://tmorris.net/
> >
> >
>
> ------------------------------------------------------------------------
> Use Hotmail to send and receive mail from your different email
> accounts. Find out how.
Re: Scaladoc that is actually useful?
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:
Re: Fwd: Scaladoc that is actually useful?
עיין מהר"ל ורמח"ל
Re: Fwd: Scaladoc that is actually useful?
There is an disjoint dichotomy drawn between "the mathematical concept
of functions" and the desire to "people who make a living by getting
computers to perform various tasks..."
Nothing could be further from the truth.
Naftoli Gugenheim wrote:
> I think that answer amounts to circular logic. :) If I misunderstood
> please expand.
>
> On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris > wrote:
>
> False dichotomy.
>
> Naftoli Gugenheim wrote:
> > In any case, Tony, you seeming to be working with the mathematical
> > concept of functions (which I have not studied). I don't think the
> > Scaladoc is geared to students of mathematical theory, but to people
> > who make a living by getting computers to perform various tasks
> (or do
> > so as a hobby), and who feel that they can do so more productively
> > with Scala, with which they are not completely familiar.
> >
> >
> > On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz
>
> > >> wrote:
> >
> > On Thursday November 12 2009, Brian Maso wrote:
> > > From: Brian Maso
> > >>
> > > Date: Thu, Nov 12, 2009 at 3:51 PM
> > > Subject: Re: [scala-user] Scaladoc that is actually useful?
> > > To: Randall R Schulz >>
> > >
> > > The following two methods have the signature (Int =>
> String) =>
> > > (String => Long) => Long, but return different values.
> Doesn't this
> > > case demonstrate you're not correct?
> >
> > It does not. The type parameters A, B and C are (implicitly)
> > universally
> > quantified. They range over _all_ types. So you can't just
> concoct
> > something and claim it's consistent with the signature of
> the function
> > in question.
> >
> >
> > > ...
> > >
> > > Best regards,
> > > Brian Maso
> >
> >
> > Randall Schulz
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>
Re: Fwd: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 7:44 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
Re: Fwd: Scaladoc that is actually useful?
If they are familiar with what I prefer to call "computer programming"
(not mathematical theory), then they are certainly more effective when
using Scala. Heck, they at least save time by not writing comments on
their composition function!
Sadly, you have produced yet another false dichotomy between mathematics
and reality. Again, nothing could be further from the truth.
How about we get back to that ever-elusive reality?
Naftoli Gugenheim wrote:
> I understood what you were referring to. What I do not see is what
> they have in common with each other.
> Mathematically, it may be a false dichotomy, but in reality people do
> not need to be familiar with function theory to program in Scala.
>
> On Thu, Nov 12, 2009 at 7:44 PM, Tony Morris > wrote:
>
> There is an disjoint dichotomy drawn between "the mathematical concept
> of functions" and the desire to "people who make a living by getting
> computers to perform various tasks..."
>
> Nothing could be further from the truth.
>
> Naftoli Gugenheim wrote:
> > I think that answer amounts to circular logic. :) If I misunderstood
> > please expand.
> >
> > On Thu, Nov 12, 2009 at 7:24 PM, Tony Morris
>
> > >> wrote:
> >
> > False dichotomy.
> >
> > Naftoli Gugenheim wrote:
> > > In any case, Tony, you seeming to be working with the
> mathematical
> > > concept of functions (which I have not studied). I don't
> think the
> > > Scaladoc is geared to students of mathematical theory, but
> to people
> > > who make a living by getting computers to perform various
> tasks
> > (or do
> > > so as a hobby), and who feel that they can do so more
> productively
> > > with Scala, with which they are not completely familiar.
> > >
> > >
> > > On Thu, Nov 12, 2009 at 6:54 PM, Randall R Schulz
> >
> >
> > >
> >>> wrote:
> > >
> > > On Thursday November 12 2009, Brian Maso wrote:
> > > > From: Brian Maso
> > >
> > >
> > >>>
> > > > Date: Thu, Nov 12, 2009 at 3:51 PM
> > > > Subject: Re: [scala-user] Scaladoc that is actually
> useful?
> > > > To: Randall R Schulz
> > >
>
> > >>>
> > > >
> > > > The following two methods have the signature (Int =>
> > String) =>
> > > > (String => Long) => Long, but return different values.
> > Doesn't this
> > > > case demonstrate you're not correct?
> > >
> > > It does not. The type parameters A, B and C are
> (implicitly)
> > > universally
> > > quantified. They range over _all_ types. So you can't just
> > concoct
> > > something and claim it's consistent with the signature of
> > the function
> > > in question.
> > >
> > >
> > > > ...
> > > >
> > > > Best regards,
> > > > Brian Maso
> > >
> > >
> > > Randall Schulz
> > >
> > >
> >
> > --
> > Tony Morris
> > http://tmorris.net/
> >
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>
Re: Scaladoc that is actually useful?
2009/11/13 Randall R Schulz :
> On Thursday November 12 2009, Dimitris Andreou wrote:
>> 2009/11/13 Tony Morris :
>> > Rex,
>> > I can read your code just fine. I assure you, the signature given
>> > is once-inhabited. There is even a proof of this fact. It's a well
>> > understood basic fact of computational theory.
>>
>> The problem is that a signature never captures the implicit "world"
>> argument that all functions have (otherwise, please show me your
>> functions having the "world" argument from which you access all of
>> scala libraries) . So the signature definitely has *not* just one
>> instance, but infinitely many.
>
> Functions are self-contained and pure. They know not of the world, other
> than that portion of the world of mathematics that defines them.
>
> A subroutine / method that accesses values not passed to it as arguments
> does not compute a function. A method that produces different values
> when called repeatedly with the same arguments does not compute a
> function.
Why? The world could contain a different B=>C function, and the method
could be using that one instead of the exlicit B=>C argument of it,
while still being a function.
>
> Not all methods compute functions. And not all signatures are "singly
> occupied," and such signatures clearly demand further characterization.
>
>
>> If you don't assume that a function is able to compute other
>> functions, just because it didn't have them as arguments, you talk
>> about something else but definitely not about scala programming. May
>> I remind that the discussion is about _scala_ docs.
>
> It is true Scala programs can readily transgress functional strictures,
> but when you say this:
>
> def func[A, B, C](f: A => B, g: B => C): A => C
>
> you've said enough.
>
> It is perfectly correct that to say more (in natural language) is either
> redundant or erroneous. Of course, while redundancy isn't a cardinal
> sin, erroneousness is.
>
> So tread carefully. Natural language, including "meaningful names" has
> equal power to mislead as to enlighten. Formal language is either
> understood or not understood. It cannot lie or mislead through
> unintended connotations.
>
>
>> This point has already been made by Rex but lets try it again :)
>
> Programmers have repeatedly been guilty of butchering established
> concepts and terminology. Calling something a function that does not
> conform to the definition of function universally agreed upon by
> mathematicians is inexcusable.
>
>
>> Regards,
>> Dimitris
>
>
> Randall Schulz
>
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
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
Re: Scaladoc that is actually useful?
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
Re: Scaladoc that is actually useful?
On Fri, Nov 13, 2009 at 3:00 AM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:
--
Daniel C. Sobral
Veni, vidi, veterni.
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
Re: Scaladoc that is actually useful?
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.
Re: Scaladoc that is actually useful?
On Fri, Nov 13, 2009 at 12:17 PM, Rex Kerr <ichoran [at] gmail [dot] com> wrote:
--
Daniel C. Sobral
Veni, vidi, veterni.
Re: Scaladoc that is actually useful?
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
Re: Scaladoc that is actually useful?
On Fri, Nov 13, 2009 at 10:25:01AM -0500, Rex Kerr said
> On Fri, Nov 13, 2009 at 9:33 AM, Daniel Sobral wrote:
>
> > Scala recommends not using isInstanceOf/asInstanceOf, because you may
> > accidentally lie about types when you use them.
> >
> > Which proves the point.
> >
>
> No, all it proves is that you can misuse the constructs that have been
> supplied.
>
> If you use them to make a whenInstanceOf construct:
>
> def whenInstanceOf[A,B,C](a:A)(f:B=>C):Option[C] = {
> if (a.isInstanceOf[B]) Some(f(a.asInstanceOf[B]))
> else None
> }
>
> then you're perfectly typesafe at least as far as set-inclusion goes, unless
> "isInstanceOf" can't manage to tell what set an object belongs to.
Bzzt.
scala> def whenInstanceOf[A,B,C](a:A)(f:B=>C):Option[C] = {
| if (a.isInstanceOf[B]) Some(f(a.asInstanceOf[B]))
| else None
| }
warning: there were unchecked warnings; re-run with -unchecked for
details
whenInstanceOf: [A,B,C](A)((B) => C)Option[C]
scala> whenInstanceOf(123){x:String => x}
java.lang.ClassCastException: java.lang.Integer cannot be cast to
java.lang.String
Ignoring the possibility of using a manifest to recover a runtime type
of B, or some hypothetical runtime with built-in reification of type
parameters.
forall A. B. C. A => (B=>C) => Option[C] is inhabited only by
None.
The forall qualifier of a type parameter truly means that the body of
the method has no information about the concrete type of any values of
the parameterized type. Therefore, any dynamic type-checks within a
method subvert the method's signature. Yes, these sorts of things can
be useful in practice, but they are abhorrent from the point of view of
static type safety, Curry-Howard correspondence, etc.
>
> 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,
Nothing could be further from the truth. It is impossible to write a
mathematical function f(x) that maps x in some unknown set A to a value
in some other unknown set B. You cannot ask a number what set it belongs
to! In fact set B could be the empty set, what then.
> 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.
For the record, I believe that everyone here just wants to help broaden
your understanding of what types really mean. No amount of API
documentation will confer that knowledge. This thread is more a
statement that what the type of a method proves about the behavior is
more important than and must be understood before some prose description
of the function that may be incorrect or incomplete.
Re: Scaladoc that is actually useful?
Geoff Reedy wrote:
>
> For the record, I believe that everyone here just wants to help broaden
> your understanding of what types really mean.
>
Well, no actually. I don't have any interest in that, and would really
rather help explore his original
question about documenting Scala-as-it-actually-exists. The results of
that are likely to be a lot more
valuable than whatever agenda y'all are pursuing.
--Dave Griffith
Re: Scaladoc that is actually useful?
Ugh, yes, I forgot about erasure making asInstanceOf half-useless. Fine. Replace with a cast and return None instead if you catch the ClassCastException. Any of that is valid inside a mathematical function. It's just a set mapping inputs to outputs. Any way you can come up with an output--including random generation--is completely fine. (Maybe it's not useful to build functions that way, but it doesn't make it not-a-function.)
I've not argued that--I'm only arguing that type theory gives a different idea of a function from mathematics. It restricts it to avoid things that are "abhorrent from the point of view of static type safety".
I already have a function that does this--the question is whether I can intercept values from set A and change them *in some cases*. It depends on what the function is allowed to know. Suppose we have a set
F(A,B) = { f : A -> B }
and a set of composable functions
CF2(A,B,C) = { (f1,f2) | f1 in F(A,B) & f2 in F(B,C) }
and
c = { ((f1,f2) in CF2(A,B,C) , g in F(A,C)) | A,B,C are sets and foreach (f1,f2) there exists unique ((f1,f2),g) }
then it *doesn't matter* how I come up with elements of F(A,C). In particular, if I happen to notice that in one special case the set C contains the string "Constant" and in such cases g is always the mapping from A to "Constant", c is still a function from CF2 to F.
Now, depending on how you construct things, you can make it so that you _cannot tell_ whether an element belongs to one set or another--if you throw away the idea of the universal set (and set complement). I can't quite tell from the axioms of constructive type theory whether or not this is true there (I believe is true; there is no universal set).
Normally, in set theory with universal sets, you can divide functions into special cases based upon the set into which the argument falls. For example, if f1 is a function from the reals to the rationals, and f2 is from the rationals to the elements of Z9, I could have a special case for my function c that always returned just the numerator of the rational.
And it turns out that the JVM can tell perfectly well which type is which, even if you need to catch an exception when things go awry.
--Rex
Re: Scaladoc that is actually useful?
On Friday November 13 2009, Geoff Reedy wrote:
> On Fri, Nov 13, 2009 at 10:25:01AM -0500, Rex Kerr said
> ...
>
> For the record, I believe that everyone here just wants to help
> broaden your understanding of what types really mean. No amount of
> API documentation will confer that knowledge. This thread is more a
> statement that what the type of a method proves about the behavior is
> more important than and must be understood before some prose
> description of the function that may be incorrect or incomplete.
Bingo!
And for my addition to the record, I _do not_ claim good understanding
of these things, but I made what "contributions" I did to this thread
in equal parts to force myself to think about what's afoot and to
convey that understanding (modulo necessary corrections) to anyone else
who cares.
I also feel the ongoing and seemingly perpetual pull of
that "pragmatism" Tony so decries. But given the sorry state of
software in general and the obvious fact that my own could be immensely
improved if I understood these things better, I must keep pushing to
understand this stuff until it finally permeates my thick skull.
Re: Scaladoc that is actually useful?
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
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
>
>
Re: Scaladoc that is actually useful?
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:
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.
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.
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
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
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/
>
>
>
Re: Scaladoc that is actually useful?
You seem to have overlooked some important parts. I will repeat them for
a third time:
* No subverting the types
* Assume termination
*crosses fingers*
Dimitris Andreou wrote:
> 2009/11/13 Tony Morris :
>
>> I did. I'm not sure what to do about the fact that you have failed to
>> see that.
>>
>
> I hope that was *not* your favourite line as a lecturer :)
>
> This is the signature I see you gave:
> def boo[A, B, C](f: A => B, g: B => C): A => C
>
> It does not constrain "boo" (scala) implementations from using the
> implicit world. So you did not address my request. If you gave another
> signature I missed, please repeat.
>
> Dimitris
>
>
>> Dimitris Andreou wrote:
>>
>>> As I said, please give us a scala signature that constrains its body
>>> from not using the world. Otherwise, I would be very happy to see how
>>> exactly you encode the mathematical signature into a scala signature
>>> which also has just one implementation. Thank you.
>>>
>>> 2009/11/13 Tony Morris :
>>>
>>>
>>>> It's entirely possible to construct a de-facto world state. The
>>>> signature definitely does have just one instance. It definitely does.
>>>> There is a proof. The strongest possible claim about reality exists.
>>>> There's not much I can do about the fact that you are refuting a proof
>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>> not even a debate.
>>>>
>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>> aware that Scala does not have an effect system. The question arises,
>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>> made this point -- *I* have already made this point.
>>>>
>>>> I will repeat myself:
>>>> (A => B) => (B => C) => A => C
>>>>
>>>> No subverting the types, assume termination --> once-inhabited!
>>>>
>>>> I am exhausted, you win.
>>>>
>>>> Dimitris Andreou wrote:
>>>>
>>>>
>>>>> 2009/11/13 Tony Morris :
>>>>>
>>>>>
>>>>>
>>>>>> Rex,
>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>> understood basic fact of computational theory.
>>>>>>
>>>>>>
>>>>>>
>>>>> The problem is that a signature never captures the implicit "world"
>>>>> argument that all functions have (otherwise, please show me your
>>>>> functions having the "world" argument from which you access all of
>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>> instance, but infinitely many.
>>>>>
>>>>> If you don't assume that a function is able to compute other
>>>>> functions, just because it didn't have them as arguments, you talk
>>>>> about something else but definitely not about scala programming. May I
>>>>> remind that the discussion is about _scala_ docs.
>>>>>
>>>>> This point has already been made by Rex but lets try it again :)
>>>>>
>>>>> Regards,
>>>>> Dimitris
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>> with -> symbol.
>>>>>>
>>>>>> Let's draw the truth table for implication:
>>>>>> P Q P->Q
>>>>>> 0 0 1
>>>>>> 0 1 1
>>>>>> 1 0 0
>>>>>> 1 1 1
>>>>>>
>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>
>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>
>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>
>>>>>> I really hope this helps. This is exhausting.
>>>>>>
>>>>>>
>>>>>> Rex Kerr wrote:
>>>>>>
>>>>>>
>>>>>>
>>>>>>> Tony,
>>>>>>>
>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>
>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>> exactly what the return type should be for the Double square
>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>> computes the n'th Fibonacci number.
>>>>>>>
>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>> on the basis of solid principles.
>>>>>>>
>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>
>>>>>>> --Rex
>>>>>>>
>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>> > wrote:
>>>>>>>
>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>
>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>> just make
>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>> interesting one.
>>>>>>>
>>>>>>> Rex Kerr wrote:
>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>> if foo
>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>> leaving
>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>> > might have practical utility.
>>>>>>> >
>>>>>>> > For example,
>>>>>>> >
>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>> > new (a:A) => (c:C) {
>>>>>>> > val b = f(a)
>>>>>>> > g(
>>>>>>> > b match {
>>>>>>> > case x:Int : -x
>>>>>>> > case x:Long : -x
>>>>>>> > case x:Float : -x
>>>>>>> > case x:Double: -x
>>>>>>> > case y: y
>>>>>>> > }
>>>>>>> > )
>>>>>>> > }
>>>>>>> > }
>>>>>>> >
>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>> the idea.)
>>>>>>> >
>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>> what is
>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>> what is
>>>>>>> > promised.
>>>>>>> >
>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>> one-to-one
>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>> > system is impractical.)
>>>>>>> >
>>>>>>> > --Rex
>>>>>>> >
>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>
>>>>>>> > >> wrote:
>>>>>>> >
>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>> ability to
>>>>>>> > print
>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>> legacy.
>>>>>>> >
>>>>>>> > There is only *one possible answer*.
>>>>>>> >
>>>>>>> >
>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>> --
>>>>>> Tony Morris
>>>>>> http://tmorris.net/
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>> --
>>>> Tony Morris
>>>> http://tmorris.net/
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> Tony Morris
>> http://tmorris.net/
>>
>>
>>
>>
>
>
Re: Scaladoc that is actually useful?
No, the existence of these assumptions (finally!) does not justify the
use of English for the general case.
Dimitris Andreou wrote:
> Alright, I think we can finally agree and end this peacefully. The
> signature *plus* some assumptions (encoded in perfectly good english)
> may make it once-habitated. The scala signature itself does _not_,
> since it does not by itself provide any extra assumptions. Many of us
> thought perhaps misunderstood that you were saying that the latter is
> also once-habitated by itself, so no english were needed in the
> scaladocs - while they *are* needed to make this extra claim, thus the
> debate. End of story. Is that ok with you?
>
> 2009/11/13 Tony Morris :
>
>> Please don't be dishonest. This is the *fourth time*.
>>
>> Let's restate the assumptions:
>>
>> * Assume termination
>> * No subverting the types
>>
>> Dimitris Andreou wrote:
>>
>>> 2009/11/13 Tony Morris :
>>>
>>>
>>>> Actually, I didn't claim that at all.
>>>>
>>>>
>>> Erm... "I assure you, the signature given is once-inhabited" - and you
>>> kind of insisted that you were talking about scala...
>>>
>>>
>>>
>>>> For the fourth time...
>>>>
>>>> ah bugger it. And no, the halting problem does not contradict that at
>>>> all (ugh!).
>>>>
>>>>
>>> But you are right about that, of course. It doesn't take a halting
>>> problem to prove that there are non-terminating implementations (which
>>> simultaneously conform to the supposedly once-habitated signature
>>> though!), one can just create a trivial example.
>>>
>>> Bye!
>>>
>>>
>>>> Dimitris Andreou wrote:
>>>>
>>>>
>>>>> Since *you* claimed that there was only a single implementation of
>>>>> that signature, it is *you* that imply that all possible
>>>>> implementations are halting. Guess what, that's exactly what the
>>>>> halting problem contradicts :)
>>>>>
>>>>> See you! It was fun :)
>>>>> I really like you you know, but sometimes I think you just rant
>>>>> unchecked (with no suppress compiler option :) )
>>>>>
>>>>> Good night all,
>>>>> Dimitris
>>>>>
>>>>> 2009/11/13 Tony Morris :
>>>>>
>>>>>
>>>>>
>>>>>> "I am not discussing this matter any further until you have solved the
>>>>>> turing halting problem!"
>>>>>>
>>>>>> That's fine by me, I'm exhausted :) Seeya!
>>>>>>
>>>>>> Dimitris Andreou wrote:
>>>>>>
>>>>>>
>>>>>>
>>>>>>> Omg, you used...english! Please encode these constrains as a scala
>>>>>>> signature and I go home. :)
>>>>>>>
>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> You seem to have overlooked some important parts. I will repeat them for
>>>>>>>> a third time:
>>>>>>>>
>>>>>>>> * No subverting the types
>>>>>>>> * Assume termination
>>>>>>>>
>>>>>>>> *crosses fingers*
>>>>>>>>
>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>>>>>> see that.
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>>>>>
>>>>>>>>> This is the signature I see you gave:
>>>>>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>>>>>
>>>>>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>>>>>> implicit world. So you did not address my request. If you gave another
>>>>>>>>> signature I missed, please repeat.
>>>>>>>>>
>>>>>>>>> Dimitris
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>>>>>> which also has just one implementation. Thank you.
>>>>>>>>>>>
>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>>>>>> not even a debate.
>>>>>>>>>>>>
>>>>>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>>>>>
>>>>>>>>>>>> I will repeat myself:
>>>>>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>>>>>
>>>>>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>>>>>
>>>>>>>>>>>> I am exhausted, you win.
>>>>>>>>>>>>
>>>>>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> Rex,
>>>>>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>>>>>> instance, but infinitely many.
>>>>>>>>>>>>>
>>>>>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>>>>>
>>>>>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>>>>>
>>>>>>>>>>>>> Regards,
>>>>>>>>>>>>> Dimitris
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>>>>>> with -> symbol.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>>>>>> P Q P->Q
>>>>>>>>>>>>>> 0 0 1
>>>>>>>>>>>>>> 0 1 1
>>>>>>>>>>>>>> 1 0 0
>>>>>>>>>>>>>> 1 1 1
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Tony,
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> --Rex
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>>>>>> > wrote:
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>>>>>>>> just make
>>>>>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>>>>>>>> interesting one.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>>>>>>>> if foo
>>>>>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>>>>>> leaving
>>>>>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>>>>>> > might have practical utility.
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > For example,
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>>>>>>>> > val b = f(a)
>>>>>>>>>>>>>>> > g(
>>>>>>>>>>>>>>> > b match {
>>>>>>>>>>>>>>> > case x:Int : -x
>>>>>>>>>>>>>>> > case x:Long : -x
>>>>>>>>>>>>>>> > case x:Float : -x
>>>>>>>>>>>>>>> > case x:Double: -x
>>>>>>>>>>>>>>> > case y: y
>>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>>> > )
>>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>>> > }
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>>>>>> the idea.)
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>>>>>>>> what is
>>>>>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>>>>>> what is
>>>>>>>>>>>>>>> > promised.
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>>>>>> one-to-one
>>>>>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>>>>>> > system is impractical.)
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > --Rex
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> > >> wrote:
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>>>>>>>> ability to
>>>>>>>>>>>>>>> > print
>>>>>>>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>>>>>>>> legacy.
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> --
>>>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>> --
>>>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>> --
>>>>>>>>>>>> Tony Morris
>>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>> --
>>>>>>>>>> Tony Morris
>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>> --
>>>>>>>> Tony Morris
>>>>>>>> http://tmorris.net/
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>> --
>>>>>> Tony Morris
>>>>>> http://tmorris.net/
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>> --
>>>> Tony Morris
>>>> http://tmorris.net/
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> Tony Morris
>> http://tmorris.net/
>>
>>
>>
>>
>
>
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/
>
>
>
Re: Scaladoc that is actually useful?
Re: Scaladoc that is actually useful?
Omg, you used...english! Please encode these constrains as a scala
signature and I go home. :)
2009/11/13 Tony Morris :
> You seem to have overlooked some important parts. I will repeat them for
> a third time:
>
> * No subverting the types
> * Assume termination
>
> *crosses fingers*
>
> Dimitris Andreou wrote:
>> 2009/11/13 Tony Morris :
>>
>>> I did. I'm not sure what to do about the fact that you have failed to
>>> see that.
>>>
>>
>> I hope that was *not* your favourite line as a lecturer :)
>>
>> This is the signature I see you gave:
>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>
>> It does not constrain "boo" (scala) implementations from using the
>> implicit world. So you did not address my request. If you gave another
>> signature I missed, please repeat.
>>
>> Dimitris
>>
>>
>>> Dimitris Andreou wrote:
>>>
>>>> As I said, please give us a scala signature that constrains its body
>>>> from not using the world. Otherwise, I would be very happy to see how
>>>> exactly you encode the mathematical signature into a scala signature
>>>> which also has just one implementation. Thank you.
>>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> It's entirely possible to construct a de-facto world state. The
>>>>> signature definitely does have just one instance. It definitely does.
>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>> not even a debate.
>>>>>
>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>> aware that Scala does not have an effect system. The question arises,
>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>> made this point -- *I* have already made this point.
>>>>>
>>>>> I will repeat myself:
>>>>> (A => B) => (B => C) => A => C
>>>>>
>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>
>>>>> I am exhausted, you win.
>>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> Rex,
>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>> understood basic fact of computational theory.
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>> argument that all functions have (otherwise, please show me your
>>>>>> functions having the "world" argument from which you access all of
>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>> instance, but infinitely many.
>>>>>>
>>>>>> If you don't assume that a function is able to compute other
>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>> about something else but definitely not about scala programming. May I
>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>
>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>
>>>>>> Regards,
>>>>>> Dimitris
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>> with -> symbol.
>>>>>>>
>>>>>>> Let's draw the truth table for implication:
>>>>>>> P Q P->Q
>>>>>>> 0 0 1
>>>>>>> 0 1 1
>>>>>>> 1 0 0
>>>>>>> 1 1 1
>>>>>>>
>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>
>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>
>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>
>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>
>>>>>>>
>>>>>>> Rex Kerr wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> Tony,
>>>>>>>>
>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>
>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>
>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>> on the basis of solid principles.
>>>>>>>>
>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>
>>>>>>>> --Rex
>>>>>>>>
>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>> > wrote:
>>>>>>>>
>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>
>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>> just make
>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>> interesting one.
>>>>>>>>
>>>>>>>> Rex Kerr wrote:
>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>> if foo
>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>> leaving
>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>> > might have practical utility.
>>>>>>>> >
>>>>>>>> > For example,
>>>>>>>> >
>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>> > val b = f(a)
>>>>>>>> > g(
>>>>>>>> > b match {
>>>>>>>> > case x:Int : -x
>>>>>>>> > case x:Long : -x
>>>>>>>> > case x:Float : -x
>>>>>>>> > case x:Double: -x
>>>>>>>> > case y: y
>>>>>>>> > }
>>>>>>>> > )
>>>>>>>> > }
>>>>>>>> > }
>>>>>>>> >
>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>> the idea.)
>>>>>>>> >
>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>> what is
>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>> what is
>>>>>>>> > promised.
>>>>>>>> >
>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>> one-to-one
>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>> > system is impractical.)
>>>>>>>> >
>>>>>>>> > --Rex
>>>>>>>> >
>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>
>>>>>>>> > >> wrote:
>>>>>>>> >
>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>> ability to
>>>>>>>> > print
>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>> legacy.
>>>>>>>> >
>>>>>>>> > There is only *one possible answer*.
>>>>>>>> >
>>>>>>>> >
>>>>>>>>
>>>>>>>> --
>>>>>>>> Tony Morris
>>>>>>>> http://tmorris.net/
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>
Re: Scaladoc that is actually useful?
"I am not discussing this matter any further until you have solved the
turing halting problem!"
That's fine by me, I'm exhausted :) Seeya!
Dimitris Andreou wrote:
> Omg, you used...english! Please encode these constrains as a scala
> signature and I go home. :)
>
> 2009/11/13 Tony Morris :
>
>> You seem to have overlooked some important parts. I will repeat them for
>> a third time:
>>
>> * No subverting the types
>> * Assume termination
>>
>> *crosses fingers*
>>
>> Dimitris Andreou wrote:
>>
>>> 2009/11/13 Tony Morris :
>>>
>>>
>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>> see that.
>>>>
>>>>
>>> I hope that was *not* your favourite line as a lecturer :)
>>>
>>> This is the signature I see you gave:
>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>
>>> It does not constrain "boo" (scala) implementations from using the
>>> implicit world. So you did not address my request. If you gave another
>>> signature I missed, please repeat.
>>>
>>> Dimitris
>>>
>>>
>>>
>>>> Dimitris Andreou wrote:
>>>>
>>>>
>>>>> As I said, please give us a scala signature that constrains its body
>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>> exactly you encode the mathematical signature into a scala signature
>>>>> which also has just one implementation. Thank you.
>>>>>
>>>>> 2009/11/13 Tony Morris :
>>>>>
>>>>>
>>>>>
>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>> not even a debate.
>>>>>>
>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>> made this point -- *I* have already made this point.
>>>>>>
>>>>>> I will repeat myself:
>>>>>> (A => B) => (B => C) => A => C
>>>>>>
>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>
>>>>>> I am exhausted, you win.
>>>>>>
>>>>>> Dimitris Andreou wrote:
>>>>>>
>>>>>>
>>>>>>
>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> Rex,
>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>> understood basic fact of computational theory.
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>> functions having the "world" argument from which you access all of
>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>> instance, but infinitely many.
>>>>>>>
>>>>>>> If you don't assume that a function is able to compute other
>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>
>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>
>>>>>>> Regards,
>>>>>>> Dimitris
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>> with -> symbol.
>>>>>>>>
>>>>>>>> Let's draw the truth table for implication:
>>>>>>>> P Q P->Q
>>>>>>>> 0 0 1
>>>>>>>> 0 1 1
>>>>>>>> 1 0 0
>>>>>>>> 1 1 1
>>>>>>>>
>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>
>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>
>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>
>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>
>>>>>>>>
>>>>>>>> Rex Kerr wrote:
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> Tony,
>>>>>>>>>
>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>
>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>
>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>> on the basis of solid principles.
>>>>>>>>>
>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>
>>>>>>>>> --Rex
>>>>>>>>>
>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>> > wrote:
>>>>>>>>>
>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>
>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>> just make
>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>> interesting one.
>>>>>>>>>
>>>>>>>>> Rex Kerr wrote:
>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>> if foo
>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>> leaving
>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>> > might have practical utility.
>>>>>>>>> >
>>>>>>>>> > For example,
>>>>>>>>> >
>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>> > val b = f(a)
>>>>>>>>> > g(
>>>>>>>>> > b match {
>>>>>>>>> > case x:Int : -x
>>>>>>>>> > case x:Long : -x
>>>>>>>>> > case x:Float : -x
>>>>>>>>> > case x:Double: -x
>>>>>>>>> > case y: y
>>>>>>>>> > }
>>>>>>>>> > )
>>>>>>>>> > }
>>>>>>>>> > }
>>>>>>>>> >
>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>> the idea.)
>>>>>>>>> >
>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>> what is
>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>> what is
>>>>>>>>> > promised.
>>>>>>>>> >
>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>> one-to-one
>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>> > system is impractical.)
>>>>>>>>> >
>>>>>>>>> > --Rex
>>>>>>>>> >
>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>
>>>>>>>>> > >> wrote:
>>>>>>>>> >
>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>> ability to
>>>>>>>>> > print
>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>> legacy.
>>>>>>>>> >
>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>> >
>>>>>>>>> >
>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>> --
>>>>>>>> Tony Morris
>>>>>>>> http://tmorris.net/
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>> --
>>>>>> Tony Morris
>>>>>> http://tmorris.net/
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>> --
>>>> Tony Morris
>>>> http://tmorris.net/
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> Tony Morris
>> http://tmorris.net/
>>
>>
>>
>>
>
>
Re: Scaladoc that is actually useful?
Since *you* claimed that there was only a single implementation of
that signature, it is *you* that imply that all possible
implementations are halting. Guess what, that's exactly what the
halting problem contradicts :)
See you! It was fun :)
I really like you you know, but sometimes I think you just rant
unchecked (with no suppress compiler option :) )
Good night all,
Dimitris
2009/11/13 Tony Morris :
> "I am not discussing this matter any further until you have solved the
> turing halting problem!"
>
> That's fine by me, I'm exhausted :) Seeya!
>
> Dimitris Andreou wrote:
>> Omg, you used...english! Please encode these constrains as a scala
>> signature and I go home. :)
>>
>> 2009/11/13 Tony Morris :
>>
>>> You seem to have overlooked some important parts. I will repeat them for
>>> a third time:
>>>
>>> * No subverting the types
>>> * Assume termination
>>>
>>> *crosses fingers*
>>>
>>> Dimitris Andreou wrote:
>>>
>>>> 2009/11/13 Tony Morris :
>>>>
>>>>
>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>> see that.
>>>>>
>>>>>
>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>
>>>> This is the signature I see you gave:
>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>
>>>> It does not constrain "boo" (scala) implementations from using the
>>>> implicit world. So you did not address my request. If you gave another
>>>> signature I missed, please repeat.
>>>>
>>>> Dimitris
>>>>
>>>>
>>>>
>>>>> Dimitris Andreou wrote:
>>>>>
>>>>>
>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>> which also has just one implementation. Thank you.
>>>>>>
>>>>>> 2009/11/13 Tony Morris :
>>>>>>
>>>>>>
>>>>>>
>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>> not even a debate.
>>>>>>>
>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>> made this point -- *I* have already made this point.
>>>>>>>
>>>>>>> I will repeat myself:
>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>
>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>
>>>>>>> I am exhausted, you win.
>>>>>>>
>>>>>>> Dimitris Andreou wrote:
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> Rex,
>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>> instance, but infinitely many.
>>>>>>>>
>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>
>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>
>>>>>>>> Regards,
>>>>>>>> Dimitris
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>> with -> symbol.
>>>>>>>>>
>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>> P Q P->Q
>>>>>>>>> 0 0 1
>>>>>>>>> 0 1 1
>>>>>>>>> 1 0 0
>>>>>>>>> 1 1 1
>>>>>>>>>
>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>
>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>
>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>
>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> Tony,
>>>>>>>>>>
>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>
>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>
>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>
>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>
>>>>>>>>>> --Rex
>>>>>>>>>>
>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>> > wrote:
>>>>>>>>>>
>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>
>>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>>> just make
>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>>> interesting one.
>>>>>>>>>>
>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>>> if foo
>>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>>> leaving
>>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>> > might have practical utility.
>>>>>>>>>> >
>>>>>>>>>> > For example,
>>>>>>>>>> >
>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>>> > val b = f(a)
>>>>>>>>>> > g(
>>>>>>>>>> > b match {
>>>>>>>>>> > case x:Int : -x
>>>>>>>>>> > case x:Long : -x
>>>>>>>>>> > case x:Float : -x
>>>>>>>>>> > case x:Double: -x
>>>>>>>>>> > case y: y
>>>>>>>>>> > }
>>>>>>>>>> > )
>>>>>>>>>> > }
>>>>>>>>>> > }
>>>>>>>>>> >
>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>> the idea.)
>>>>>>>>>> >
>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>>> what is
>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>> what is
>>>>>>>>>> > promised.
>>>>>>>>>> >
>>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>>> one-to-one
>>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>> > system is impractical.)
>>>>>>>>>> >
>>>>>>>>>> > --Rex
>>>>>>>>>> >
>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>
>>>>>>>>>> > >> wrote:
>>>>>>>>>> >
>>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>>> ability to
>>>>>>>>>> > print
>>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>>> legacy.
>>>>>>>>>> >
>>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>>> >
>>>>>>>>>> >
>>>>>>>>>>
>>>>>>>>>> --
>>>>>>>>>> Tony Morris
>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>> --
>>>>>>>>> Tony Morris
>>>>>>>>> http://tmorris.net/
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>> --
>>>>>>> Tony Morris
>>>>>>> http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>> --
>>>>> Tony Morris
>>>>> http://tmorris.net/
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>> --
>>> Tony Morris
>>> http://tmorris.net/
>>>
>>>
>>>
>>>
>>
>>
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>
Re: Scaladoc that is actually useful?
Actually, I didn't claim that at all.
For the fourth time...
ah bugger it. And no, the halting problem does not contradict that at
all (ugh!).
Dimitris Andreou wrote:
> Since *you* claimed that there was only a single implementation of
> that signature, it is *you* that imply that all possible
> implementations are halting. Guess what, that's exactly what the
> halting problem contradicts :)
>
> See you! It was fun :)
> I really like you you know, but sometimes I think you just rant
> unchecked (with no suppress compiler option :) )
>
> Good night all,
> Dimitris
>
> 2009/11/13 Tony Morris :
>
>> "I am not discussing this matter any further until you have solved the
>> turing halting problem!"
>>
>> That's fine by me, I'm exhausted :) Seeya!
>>
>> Dimitris Andreou wrote:
>>
>>> Omg, you used...english! Please encode these constrains as a scala
>>> signature and I go home. :)
>>>
>>> 2009/11/13 Tony Morris :
>>>
>>>
>>>> You seem to have overlooked some important parts. I will repeat them for
>>>> a third time:
>>>>
>>>> * No subverting the types
>>>> * Assume termination
>>>>
>>>> *crosses fingers*
>>>>
>>>> Dimitris Andreou wrote:
>>>>
>>>>
>>>>> 2009/11/13 Tony Morris :
>>>>>
>>>>>
>>>>>
>>>>>> I did. I'm not sure what to do about the fact that you have failed to
>>>>>> see that.
>>>>>>
>>>>>>
>>>>>>
>>>>> I hope that was *not* your favourite line as a lecturer :)
>>>>>
>>>>> This is the signature I see you gave:
>>>>> def boo[A, B, C](f: A => B, g: B => C): A => C
>>>>>
>>>>> It does not constrain "boo" (scala) implementations from using the
>>>>> implicit world. So you did not address my request. If you gave another
>>>>> signature I missed, please repeat.
>>>>>
>>>>> Dimitris
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>> Dimitris Andreou wrote:
>>>>>>
>>>>>>
>>>>>>
>>>>>>> As I said, please give us a scala signature that constrains its body
>>>>>>> from not using the world. Otherwise, I would be very happy to see how
>>>>>>> exactly you encode the mathematical signature into a scala signature
>>>>>>> which also has just one implementation. Thank you.
>>>>>>>
>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>> It's entirely possible to construct a de-facto world state. The
>>>>>>>> signature definitely does have just one instance. It definitely does.
>>>>>>>> There is a proof. The strongest possible claim about reality exists.
>>>>>>>> There's not much I can do about the fact that you are refuting a proof
>>>>>>>> by simply asserting the contrary. I'd move this to scala-debate but it's
>>>>>>>> not even a debate.
>>>>>>>>
>>>>>>>> I talk about *functions* and definitely Scala programming. I'm well
>>>>>>>> aware that Scala does not have an effect system. The question arises,
>>>>>>>> what shall we do about it? The answer is not English. Rex hasn't already
>>>>>>>> made this point -- *I* have already made this point.
>>>>>>>>
>>>>>>>> I will repeat myself:
>>>>>>>> (A => B) => (B => C) => A => C
>>>>>>>>
>>>>>>>> No subverting the types, assume termination --> once-inhabited!
>>>>>>>>
>>>>>>>> I am exhausted, you win.
>>>>>>>>
>>>>>>>> Dimitris Andreou wrote:
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>> 2009/11/13 Tony Morris :
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> Rex,
>>>>>>>>>> I can read your code just fine. I assure you, the signature given is
>>>>>>>>>> once-inhabited. There is even a proof of this fact. It's a well
>>>>>>>>>> understood basic fact of computational theory.
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>> The problem is that a signature never captures the implicit "world"
>>>>>>>>> argument that all functions have (otherwise, please show me your
>>>>>>>>> functions having the "world" argument from which you access all of
>>>>>>>>> scala libraries) . So the signature definitely has *not* just one
>>>>>>>>> instance, but infinitely many.
>>>>>>>>>
>>>>>>>>> If you don't assume that a function is able to compute other
>>>>>>>>> functions, just because it didn't have them as arguments, you talk
>>>>>>>>> about something else but definitely not about scala programming. May I
>>>>>>>>> remind that the discussion is about _scala_ docs.
>>>>>>>>>
>>>>>>>>> This point has already been made by Rex but lets try it again :)
>>>>>>>>>
>>>>>>>>> Regards,
>>>>>>>>> Dimitris
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>> So, the question arises, where are you wrong? The theorem: forall A B. A
>>>>>>>>>> -> B is also known as "the cast operator." Under the Curry-Howard
>>>>>>>>>> Isomorphism, functions are implication -- that is why we denote them
>>>>>>>>>> with -> symbol.
>>>>>>>>>>
>>>>>>>>>> Let's draw the truth table for implication:
>>>>>>>>>> P Q P->Q
>>>>>>>>>> 0 0 1
>>>>>>>>>> 0 1 1
>>>>>>>>>> 1 0 0
>>>>>>>>>> 1 1 1
>>>>>>>>>>
>>>>>>>>>> So we have a premise and a conclusion in one. We see immediately that
>>>>>>>>>> this is not tautological. Therefore, forall A B. A -> B is not a
>>>>>>>>>> theorem. If you'll allow me an indulgence in quoting Erik Meijer at a
>>>>>>>>>> conference in front about ~400 typical programmers, "It is a LIE!"
>>>>>>>>>>
>>>>>>>>>> Scala's type systems has many "let's escape reality and tell lies." One
>>>>>>>>>> of them is side-effects, another is casting. Haskell, which also does
>>>>>>>>>> same, calls the former unsafePerformIO and the latter unsafeCoerce. The
>>>>>>>>>> "unsafe" prefix is intended to denote "Caution, these functions tell lies."
>>>>>>>>>>
>>>>>>>>>> The question can be phrased in English as "tell the truth about this
>>>>>>>>>> signature." This means no lies, no subverting the types. No def cast[A,
>>>>>>>>>> B](a: A): B functions allowed. To the extent that you use them is the
>>>>>>>>>> extent that you are telling lies (and so we must not get *all* our
>>>>>>>>>> documentation from types, but we should strive for it as a virtue).
>>>>>>>>>>
>>>>>>>>>> I really hope this helps. This is exhausting.
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>> Tony,
>>>>>>>>>>>
>>>>>>>>>>> I'm not convinced you're paying attention to my code, and if you are,
>>>>>>>>>>> I'm not convinced you're proposing anything sensible.
>>>>>>>>>>>
>>>>>>>>>>> Please explain exactly where the subversion occurs, and please say
>>>>>>>>>>> exactly what the return type should be for the Double square
>>>>>>>>>>> function. If the return type for the Double function is not Double,
>>>>>>>>>>> please explain what the return type is for the F(n) function which
>>>>>>>>>>> computes the n'th Fibonacci number.
>>>>>>>>>>>
>>>>>>>>>>> Or you can come up with some alternate scheme that will demonstrate
>>>>>>>>>>> that you are actually understanding what I am saying and disagreeing
>>>>>>>>>>> on the basis of solid principles.
>>>>>>>>>>>
>>>>>>>>>>> (Or, of course, we can just drop it.)
>>>>>>>>>>>
>>>>>>>>>>> --Rex
>>>>>>>>>>>
>>>>>>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris >>>>>>>>>> > wrote:
>>>>>>>>>>>
>>>>>>>>>>> You've subverted the types again. forall A B. A -> B is not a theorem.
>>>>>>>>>>>
>>>>>>>>>>> I assure you, there is only one possible solution and I didn't
>>>>>>>>>>> just make
>>>>>>>>>>> it up. I refer back to my lobbying for basic type theory in schools. I
>>>>>>>>>>> predict we wouldn't be having this discussion, but a more
>>>>>>>>>>> interesting one.
>>>>>>>>>>>
>>>>>>>>>>> Rex Kerr wrote:
>>>>>>>>>>> > There are infinitely many possible answers to what can happen with
>>>>>>>>>>> > that type signature, given that A and B can be any type. What
>>>>>>>>>>> if foo
>>>>>>>>>>> > picks out certain Bs and converts them to different B's, while
>>>>>>>>>>> leaving
>>>>>>>>>>> > everything else alone? The type system *only says that boo gives a
>>>>>>>>>>> > function that takes A and returns C*. It doesn't say anything about
>>>>>>>>>>> > how. There's an obvious path, and lots of non-obvious paths that
>>>>>>>>>>> > might have practical utility.
>>>>>>>>>>> >
>>>>>>>>>>> > For example,
>>>>>>>>>>> >
>>>>>>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
>>>>>>>>>>> > new (a:A) => (c:C) {
>>>>>>>>>>> > val b = f(a)
>>>>>>>>>>> > g(
>>>>>>>>>>> > b match {
>>>>>>>>>>> > case x:Int : -x
>>>>>>>>>>> > case x:Long : -x
>>>>>>>>>>> > case x:Float : -x
>>>>>>>>>>> > case x:Double: -x
>>>>>>>>>>> > case y: y
>>>>>>>>>>> > }
>>>>>>>>>>> > )
>>>>>>>>>>> > }
>>>>>>>>>>> > }
>>>>>>>>>>> >
>>>>>>>>>>> > (I didn't run this, so there may be syntax errors, but you get
>>>>>>>>>>> the idea.)
>>>>>>>>>>> >
>>>>>>>>>>> > This is *entirely fine* by the type system. It takes exactly
>>>>>>>>>>> what is
>>>>>>>>>>> > promised, has no side effects whatsoever, and returns exactly
>>>>>>>>>>> what is
>>>>>>>>>>> > promised.
>>>>>>>>>>> >
>>>>>>>>>>> > Sure, there are now some subset of inputs that may have had
>>>>>>>>>>> one-to-one
>>>>>>>>>>> > mappings that now are not, but that's not the type system's job to
>>>>>>>>>>> > handle. (Unless, of course, you think that def
>>>>>>>>>>> > square(x:Double):NonNegativeDouble is the proper type signature for
>>>>>>>>>>> > the x*x operation; in that case, I'd just point out that such a type
>>>>>>>>>>> > system is impractical.)
>>>>>>>>>>> >
>>>>>>>>>>> > --Rex
>>>>>>>>>>> >
>>>>>>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
>>>>>>>>>>>
>>>>>>>>>>> > >> wrote:
>>>>>>>>>>> >
>>>>>>>>>>> > Unfortunately you have subverted the types. There is no
>>>>>>>>>>> ability to
>>>>>>>>>>> > print
>>>>>>>>>>> > a universal type. This is an unfortunate part of the Java
>>>>>>>>>>> legacy.
>>>>>>>>>>> >
>>>>>>>>>>> > There is only *one possible answer*.
>>>>>>>>>>> >
>>>>>>>>>>> >
>>>>>>>>>>>
>>>>>>>>>>> --
>>>>>>>>>>> Tony Morris
>>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>> --
>>>>>>>>>> Tony Morris
>>>>>>>>>> http://tmorris.net/
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>> --
>>>>>>>> Tony Morris
>>>>>>>> http://tmorris.net/
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>> --
>>>>>> Tony Morris
>>>>>> http://tmorris.net/
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>> --
>>>> Tony Morris
>>>> http://tmorris.net/
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>> --
>> Tony Morris
>> http://tmorris.net/
>>
>>
>>
>>
>
>
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/
>
>
>
Re: Scaladoc that is actually useful?
On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris <tonymorris [at] gmail [dot] com> wrote:
Re: Scaladoc that is actually useful?
For the third time, no. No turing-complete language does. Some other
languages do -- one I have used a lot is Coq. Another is Agda. I
recommend both of these to you.
Does this mean it is not a useful question in the context of the issue
of English as a language for documentation? No it doesn't.
Naftoli Gugenheim wrote:
> Does the scala library obey those assumptions?
>
> On Thu, Nov 12, 2009 at 7:37 PM, Tony Morris > wrote:
>
> You seem to have overlooked some important parts. I will repeat
> them for
> a third time:
>
> * No subverting the types
> * Assume termination
>
> *crosses fingers*
>
> Dimitris Andreou wrote:
> > 2009/11/13 Tony Morris >:
> >
> >> I did. I'm not sure what to do about the fact that you have
> failed to
> >> see that.
> >>
> >
> > I hope that was *not* your favourite line as a lecturer :)
> >
> > This is the signature I see you gave:
> > def boo[A, B, C](f: A => B, g: B => C): A => C
> >
> > It does not constrain "boo" (scala) implementations from using the
> > implicit world. So you did not address my request. If you gave
> another
> > signature I missed, please repeat.
> >
> > Dimitris
> >
> >
> >> Dimitris Andreou wrote:
> >>
> >>> As I said, please give us a scala signature that constrains
> its body
> >>> from not using the world. Otherwise, I would be very happy to
> see how
> >>> exactly you encode the mathematical signature into a scala
> signature
> >>> which also has just one implementation. Thank you.
> >>>
> >>> 2009/11/13 Tony Morris >:
> >>>
> >>>
> >>>> It's entirely possible to construct a de-facto world state. The
> >>>> signature definitely does have just one instance. It
> definitely does.
> >>>> There is a proof. The strongest possible claim about reality
> exists.
> >>>> There's not much I can do about the fact that you are
> refuting a proof
> >>>> by simply asserting the contrary. I'd move this to
> scala-debate but it's
> >>>> not even a debate.
> >>>>
> >>>> I talk about *functions* and definitely Scala programming.
> I'm well
> >>>> aware that Scala does not have an effect system. The
> question arises,
> >>>> what shall we do about it? The answer is not English. Rex
> hasn't already
> >>>> made this point -- *I* have already made this point.
> >>>>
> >>>> I will repeat myself:
> >>>> (A => B) => (B => C) => A => C
> >>>>
> >>>> No subverting the types, assume termination --> once-inhabited!
> >>>>
> >>>> I am exhausted, you win.
> >>>>
> >>>> Dimitris Andreou wrote:
> >>>>
> >>>>
> >>>>> 2009/11/13 Tony Morris >:
> >>>>>
> >>>>>
> >>>>>
> >>>>>> Rex,
> >>>>>> I can read your code just fine. I assure you, the signature
> given is
> >>>>>> once-inhabited. There is even a proof of this fact. It's a well
> >>>>>> understood basic fact of computational theory.
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>> The problem is that a signature never captures the implicit
> "world"
> >>>>> argument that all functions have (otherwise, please show me your
> >>>>> functions having the "world" argument from which you access
> all of
> >>>>> scala libraries) . So the signature definitely has *not*
> just one
> >>>>> instance, but infinitely many.
> >>>>>
> >>>>> If you don't assume that a function is able to compute other
> >>>>> functions, just because it didn't have them as arguments,
> you talk
> >>>>> about something else but definitely not about scala
> programming. May I
> >>>>> remind that the discussion is about _scala_ docs.
> >>>>>
> >>>>> This point has already been made by Rex but lets try it again :)
> >>>>>
> >>>>> Regards,
> >>>>> Dimitris
> >>>>>
> >>>>>
> >>>>>
> >>>>>
> >>>>>> So, the question arises, where are you wrong? The theorem:
> forall A B. A
> >>>>>> -> B is also known as "the cast operator." Under the
> Curry-Howard
> >>>>>> Isomorphism, functions are implication -- that is why we
> denote them
> >>>>>> with -> symbol.
> >>>>>>
> >>>>>> Let's draw the truth table for implication:
> >>>>>> P Q P->Q
> >>>>>> 0 0 1
> >>>>>> 0 1 1
> >>>>>> 1 0 0
> >>>>>> 1 1 1
> >>>>>>
> >>>>>> So we have a premise and a conclusion in one. We see
> immediately that
> >>>>>> this is not tautological. Therefore, forall A B. A -> B is
> not a
> >>>>>> theorem. If you'll allow me an indulgence in quoting Erik
> Meijer at a
> >>>>>> conference in front about ~400 typical programmers, "It is
> a LIE!"
> >>>>>>
> >>>>>> Scala's type systems has many "let's escape reality and
> tell lies." One
> >>>>>> of them is side-effects, another is casting. Haskell, which
> also does
> >>>>>> same, calls the former unsafePerformIO and the latter
> unsafeCoerce. The
> >>>>>> "unsafe" prefix is intended to denote "Caution, these
> functions tell lies."
> >>>>>>
> >>>>>> The question can be phrased in English as "tell the truth
> about this
> >>>>>> signature." This means no lies, no subverting the types. No
> def cast[A,
> >>>>>> B](a: A): B functions allowed. To the extent that you use
> them is the
> >>>>>> extent that you are telling lies (and so we must not get
> *all* our
> >>>>>> documentation from types, but we should strive for it as a
> virtue).
> >>>>>>
> >>>>>> I really hope this helps. This is exhausting.
> >>>>>>
> >>>>>>
> >>>>>> Rex Kerr wrote:
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>> Tony,
> >>>>>>>
> >>>>>>> I'm not convinced you're paying attention to my code, and
> if you are,
> >>>>>>> I'm not convinced you're proposing anything sensible.
> >>>>>>>
> >>>>>>> Please explain exactly where the subversion occurs, and
> please say
> >>>>>>> exactly what the return type should be for the Double square
> >>>>>>> function. If the return type for the Double function is
> not Double,
> >>>>>>> please explain what the return type is for the F(n)
> function which
> >>>>>>> computes the n'th Fibonacci number.
> >>>>>>>
> >>>>>>> Or you can come up with some alternate scheme that will
> demonstrate
> >>>>>>> that you are actually understanding what I am saying and
> disagreeing
> >>>>>>> on the basis of solid principles.
> >>>>>>>
> >>>>>>> (Or, of course, we can just drop it.)
> >>>>>>>
> >>>>>>> --Rex
> >>>>>>>
> >>>>>>> On Thu, Nov 12, 2009 at 6:10 PM, Tony Morris
>
> >>>>>>> >> wrote:
> >>>>>>>
> >>>>>>> You've subverted the types again. forall A B. A -> B
> is not a theorem.
> >>>>>>>
> >>>>>>> I assure you, there is only one possible solution and
> I didn't
> >>>>>>> just make
> >>>>>>> it up. I refer back to my lobbying for basic type
> theory in schools. I
> >>>>>>> predict we wouldn't be having this discussion, but a more
> >>>>>>> interesting one.
> >>>>>>>
> >>>>>>> Rex Kerr wrote:
> >>>>>>> > There are infinitely many possible answers to what
> can happen with
> >>>>>>> > that type signature, given that A and B can be any
> type. What
> >>>>>>> if foo
> >>>>>>> > picks out certain Bs and converts them to different
> B's, while
> >>>>>>> leaving
> >>>>>>> > everything else alone? The type system *only says
> that boo gives a
> >>>>>>> > function that takes A and returns C*. It doesn't
> say anything about
> >>>>>>> > how. There's an obvious path, and lots of
> non-obvious paths that
> >>>>>>> > might have practical utility.
> >>>>>>> >
> >>>>>>> > For example,
> >>>>>>> >
> >>>>>>> > def boo[A,B,C](f: A => B, g: B => C) : A => C = {
> >>>>>>> > new (a:A) => (c:C) {
> >>>>>>> > val b = f(a)
> >>>>>>> > g(
> >>>>>>> > b match {
> >>>>>>> > case x:Int : -x
> >>>>>>> > case x:Long : -x
> >>>>>>> > case x:Float : -x
> >>>>>>> > case x:Double: -x
> >>>>>>> > case y: y
> >>>>>>> > }
> >>>>>>> > )
> >>>>>>> > }
> >>>>>>> > }
> >>>>>>> >
> >>>>>>> > (I didn't run this, so there may be syntax errors,
> but you get
> >>>>>>> the idea.)
> >>>>>>> >
> >>>>>>> > This is *entirely fine* by the type system. It
> takes exactly
> >>>>>>> what is
> >>>>>>> > promised, has no side effects whatsoever, and
> returns exactly
> >>>>>>> what is
> >>>>>>> > promised.
> >>>>>>> >
> >>>>>>> > Sure, there are now some subset of inputs that may
> have had
> >>>>>>> one-to-one
> >>>>>>> > mappings that now are not, but that's not the type
> system's job to
> >>>>>>> > handle. (Unless, of course, you think that def
> >>>>>>> > square(x:Double):NonNegativeDouble is the proper
> type signature for
> >>>>>>> > the x*x operation; in that case, I'd just point out
> that such a type
> >>>>>>> > system is impractical.)
> >>>>>>> >
> >>>>>>> > --Rex
> >>>>>>> >
> >>>>>>> > On Thu, Nov 12, 2009 at 5:12 PM, Tony Morris
> >>>>>>>
> >
> >>>>>>> > >>> wrote:
> >>>>>>> >
> >>>>>>> > Unfortunately you have subverted the types.
> There is no
> >>>>>>> ability to
> >>>>>>> > print
> >>>>>>> > a universal type. This is an unfortunate part of
> the Java
> >>>>>>> legacy.
> >>>>>>> >
> >>>>>>> > There is only *one possible answer*.
> >>>>>>> >
> >>>>>>> >
> >>>>>>>
> >>>>>>> --
> >>>>>>> Tony Morris
> >>>>>>> http://tmorris.net/
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>> --
> >>>>>> Tony Morris
> >>>>>> http://tmorris.net/
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>>>>
> >>>> --
> >>>> Tony Morris
> >>>> http://tmorris.net/
> >>>>
> >>>>
> >>>>
> >>>>
> >>>>
> >>>
> >> --
> >> Tony Morris
> >> http://tmorris.net/
> >>
> >>
> >>
> >>
> >
> >
>
> --
> Tony Morris
> http://tmorris.net/
>
>
>