Benefits of static typing
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Where I work, I use Haskell mostly. I use Scala second-mostly and
other languages such as Java, Javascript and others rarely. Regardless
of language, I use high-level techniques for implementing our business
solutions.
I also do teaching at work. I use Haskell for teaching almost
exclusively. Occasionally Scala, Java or C# when a point may be better
understood in that context. I also do teaching voluntarily. Every
Tuesday, about 5 of use meet in a room to learn. The structure of the
learning material is similar in both cases. I used to do "teaching" at
university, but it is nothing like what I do now -- today I set the
curriculum geared specifically toward learning with no other agenda
and alter it according to new things I learn about teaching.
Having done this for years, I tend to see the same questions and
misunderstandings. This means I can start making predictions about a
student's progress. This confidence in prediction was recently broken
a little. Let me tell you why.
I gave the students a problem. Since giving it to them, I have altered
the problem slightly, but I do not expect this alteration to change
the outcome (of course, surprises at every turn). I will give you the
altered version.
Write an API for tic-tac-toe. Do not use variables -- they are not
permitted -- this includes libraries that expose in-line updates. No
exceptions (or non-termination) in exposed functions -- all functions
return a consistent value for every element of their domain. The
follow API methods should exist:
* move: takes a tic-tac-toe board and position and moves to that
position (if not occupied) returning a new board. This function can
only be called on a board that is in-play. Calling move on a game
board that is finished is a *compile-time type error*.
* whoWon: takes a tic-tac-toe board and returns the player that won
the game (or a draw if neither). This function can only be called on a
board that is finished. Calling move on a game board that is in-play
is a *compile-time type error*.
* takeBack: takes either a finished board or a board in-play that has
had at least one move and returns a board in-play. It is a
compile-time type error to call this function on an empty board.
* playerAt: takes a tic-tac-toe board and position and returns the
(possible) player at a given position. This function works on any type
of board.
* Other API functions that you may see fit. These can be determined by
also writing a console application that uses the API -- other useful
functions are likely to arise.
You should write automated tests for your API. For example, the
following universally quantified property holds true:
forall Board b. forall Position p. such that (not (positionIsOccupied
p b)). takeBack(move(p, b)) == b
You should encode this property in a test. For Scala, use ScalaCheck.
For Haskell, QuickCheck.
When I gave this problem to students, I predicted an outcome of how
difficult this would be for students to achieve. It has turned out on
all occasions (both at work and teaching voluntarily) that this has
proven far more difficult than I predicted. I am forced to consider
that either my selection sample is skewed or my understanding of
learning programming needs revision. I would love for more data on
this or even better, rigorous scientific studies on learning in a
programming context in general. I digress.
Regardless of my slight loss of confidence, I still quite certain that
this exercise is excellent for understanding some of the practical
implications of software correctness verification and may even serve
as a reasonable means by which to introduce students to more advanced
topics such as dependent types and general type theory. The practical
implications are especially appealing to my colleagues who work in L3
support and receive phone calls about an API that was called by a
client, which broke everything. Consider the fact that this is *simply
impossible* with a well designed, machine-verification-checked API.
You are invited to attempt this exercise for yourself, even if for
your own personal challenge. I cannot guarantee that you will learn
something about static typing today, but I would have guaranteed that
to you a few weeks ago. I am now on the fence, so to speak. I have
solved this problem with both Scala and Haskell. It would be difficult
to do in Java without library support such as Functional Java (you'd
end up spending a lot of time rewriting it) and even then. Functional
Java also includes automated testing support.
I hope this helps.
PS: This is not really a debate invitation, but I figure [scala-user]
is a bit overloaded at the moment. Enjoy!
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1TIuMACgkQmnpgrYe6r633mgCgkC457i8OPby1VUzM8n40tnse
tkgAoMMBPl4jbH/z2xM5M62kqewVb/tk
=fGJB
-----END PGP SIGNATURE-----
Stefan Wachter
could you please recommend some study material that could help solving
that exercise. Can you recommend other introductory or advanced text books.
Thanks
Stefan
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
There is not really anything specific that will help you solve this
problem, except for a few neat little programming tricks. One of these
is called "smart constructors" or perhaps a variation of "the factory
design pattern."
Consider for example, a data type that holds only natural numbers. We
might represent this as an Int, (or the church encoding, but let's not
go there) but this is unsafe for negative values. So we might write
our own unsafe code but enforce the invariant to our exposed API. This
is one of many reasons why no variables are allowed, since doing this
trick without that can be very difficult.
case class Natural(n: Int) // this won't cut it, since the API caller
may do Natural(-1).
However, here is a way of encoding smart constructors in scala. Note
the add method below.
// note: sealed
sealed trait Natural {
val value: Int
def add = {
// WARNING: unsafe internal call
case Natural(n) => Natural.unsafeNatural(value + n)
}
}
object Natural {
// Note private. Only useful for our internal code
private def unsafeNatural(n: Int): Natural
def natural(n: Int): Option[Natural] = ... // note Option
def naturalOr(n: Int, nat: => Natural) = natural(n) getOrElse nat
// other useful constructors, but no unsafe ones!
}
Instead of Int/Natural, you'll be doing things with different types of
Board, performing unsafe calls inside your implementation, but
disallowing it from the client code just as the add method does here.
As a side note, I also know of one person (I know him personally) who
is implementing this exercise so that even internal calls are safe,
however, he is using a dependently-typed language called Coq (he is
also self-admittedly obsessed with these kinds of exercises).
Another useful technique for your Scala solution is the use of
implicits or traits. Specifically, to provide methods that are common
to more than one data type.
Hope this helps. Let me know if you have more questions.
On 10/02/11 18:38, Stefan Wachter wrote:
>
> could you please recommend some study material that could help
> solving that exercise. Can you recommend other introductory or
> advanced text books.
>
> Thanks
>
> Stefan
>
>
>
>>
>>
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
rMgAnjtzK5Jb8O4nFqQ4LVO8CGXUy1z1
=JX+S
-----END PGP SIGNATURE-----
Rex Kerr
When I gave this problem to students, I predicted an outcome of how
difficult this would be for students to achieve. It has turned out on
all occasions (both at work and teaching voluntarily) that this has
proven far more difficult than I predicted. I am forced to consider
that either my selection sample is skewed or my understanding of
learning programming needs revision. I would love for more data on
this or even better, rigorous scientific studies on learning in a
programming context in general.
I don't know if a single data point helps any, but I find the solution highly nonobvious, mostly because there are readily apparent brute-force methods to solve the problem which are nonetheless highly unsatisfying. Still, it seems as though the solution necessitates some degree of brute force (i.e. meaningless repetition of types where a more compact representation would use variables).
In particular, requiring compile-time errors for moving on completed boards means that the type system has to not only know the number of moves on the board but exactly what those moves were, and be able to recognize that the five-move pattern
XXX
OO-
---
is a terminal type, whereas
XOX
XO-
---
is not, despite the players having made the same number of moves each. Asking the type system to do this sort of computation seems awkward at best, and leads me at least to reject every potential solution I've come up with so far as unworkable.
Of course, writing an API might not be so hard depending on what you mean by "returns". If "either" counts as returning a board, then it gets tolerably easy to write the API since you can put the game-end-detection logic into the code rather than the type system.
And it's possible that some elegant solution to this problem does exist, but if so, you now have another data point confirming its non-obviousness.
--Rex
Alec Zorab
over or not, and return one of PlayableBoard or FinishedBoard?
Jim Powers
wheelhouse than Scala's, but that should not surprise anyone,
especially Mr. Morris. ;-)
OK, I'm almost done (I think) but I do have a question about
"variables". Do you mean local "let" bindings (vals in Scala) are
verboten? Or just actual "variables" (vars in Scala) are off-limits.
--
Jim Powers
Dennis Haupt
val x = something
can be simulated by
methodcall(something)
and
def methodcall(x:Something) {
//the "local" val is implemented as a method parameter
}
i see no reason why you should not be allowed to use local variables.
-------- Original-Nachricht --------
> Datum: Thu, 10 Feb 2011 08:18:02 -0800 (PST)
> Von: Jim Powers <j...@casapowers.com>
> An: scala-debate <scala-...@googlegroups.com>
> Betreff: [scala-debate] Re: Benefits of static typing
Jim Powers
> since
>
> val x = something
>
> can be simulated by
>
> methodcall(something)
> and
> def methodcall(x:Something) {
> //the "local" val is implemented as a method parameter
>
> }
>
> i see no reason why you should not be allowed to use local variables.
x>).
I think the intent it to use strictly "non-update-able" identifiers.
In Haskell there is no way to update a binding (they're not called
"variables" because a particular identifier's value does not "vary" -
there are no "vars" in Haskell). I guess the point of clarification I
was seeking was: "If you are going to introduce a local binding then
you must do so via function application." Which I agree with you ought
to be unnecessary since I'm sure the point of the exercise is to show
how using algebraic data types in a purely functional manner can
produce an elegant, concise, and correct solution to this problem.
Not "there is no need for the syntactic sugar of local let binding
forms (along with where binding forms in Haskell) because all such
nonsense can be gotten through function application". Just checking.
Steven Obua
Russ P.
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Where I work, I use Haskell mostly. I use Scala second-mostly and
> other languages such as Java, Javascript and others rarely. Regardless
> of language, I use high-level techniques for implementing our business
> solutions.
>
> I also do teaching at work. I use Haskell for teaching almost
> exclusively. Occasionally Scala, Java or C# when a point may be better
> understood in that context. I also do teaching voluntarily. Every
> Tuesday, about 5 of use meet in a room to learn. The structure of the
> learning material is similar in both cases. I used to do "teaching" at
> university, but it is nothing like what I do now -- today I set the
> curriculum geared specifically toward learning with no other agenda
> and alter it according to new things I learn about teaching.
I assume that this post was in reply to my question, although you did
not quote it (and your post somehow got orphaned off onto a separate
topic.)
That's all interesting, but you did not answer my questions. I wanted
to know if you think Scala has any inherent advantages over Haskell
(i.e., advantages other than popularity). I was also curious about
whether you think the object-oriented features of Scala have a
legitimate use or whether you think Scala should preferably always be
used as a pure functional language.
I can more or less infer the answers from your posts. The impression I
get is that you consider the object-oriented feature of Scala to be a
corruption of the true functional paradigm. If that is really what you
think, then you probably consider Haskell purer than Scala and
therefore superior to Scala.
Why do I care what you think? I figure you are probably representative
of functional programming purists in general. If I understand your
position correctly, you think that the object-oriented features of
Scala, and variables and mutability in general, are concessions to bad
programmers and sloppy programming practices.
I am interested in developing reliable software for a safety-critical
application, and I am wondering if it makes sense to try for a purely
functional design. To be honest, I don't think I can get there, but I
would like to know if it is even a sensible goal.
--Russ P.
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
On 11/02/11 00:43, Rex Kerr wrote:
> On Wed, Feb 9, 2011 at 6:27 PM, Tony Morris <tonym...@gmail.com> wrote:
>
>>
>> When I gave this problem to students, I predicted an outcome of how
>> difficult this would be for students to achieve. It has turned out on
>> all occasions (both at work and teaching voluntarily) that this has
>> proven far more difficult than I predicted. I am forced to consider
>> that either my selection sample is skewed or my understanding of
>> learning programming needs revision. I would love for more data on
>> this or even better, rigorous scientific studies on learning in a
>> programming context in general.
>
>
> I don't know if a single data point helps any, but I find the solution
> highly nonobvious, mostly because there are readily apparent brute-force
> methods to solve the problem which are nonetheless highly unsatisfying.
> Still, it seems as though the solution necessitates some degree of brute
> force (i.e. meaningless repetition of types where a more compact
> representation would use variables).
This would lose points. Code repetition is not necessitated.
>
> In particular, requiring compile-time errors for moving on completed boards
> means that the type system has to not only know the number of moves on the
> board but exactly what those moves were, and be able to recognize that the
> five-move pattern
> XXX
> OO-
> ---
> is a terminal type, whereas
> XOX
> XO-
> ---
> is not, despite the players having made the same number of moves each.
> Asking the type system to do this sort of computation seems awkward at
best,
> and leads me at least to reject every potential solution I've come up with
> so far as unworkable.
Scala is not a dependently-typed language. You will need to write
unsafe code but not expose that ability to your clients. In other
words, you will be saying to your clients, "I promise this works,
always", though with significantly higher confidence than your typical
API design. Like I said, I have a friend solving this with Coq, where
he will be saying, "it is a fact that this work, regardless of any
promises I might make."
>
> Of course, writing an API might not be so hard depending on what you
mean by
> "returns". If "either" counts as returning a board, then it gets tolerably
> easy to write the API since you can put the game-end-detection logic into
> the code rather than the type system.
Adjust the API to suit the problem.
>
> And it's possible that some elegant solution to this problem does
exist, but
> if so, you now have another data point confirming its non-obviousness.
Thanks.
>
> --Rex
>
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1UUtcACgkQmnpgrYe6r60wqgCfW7K643rjQrbFutz2f4GZg7A8
OdkAmgJRujmKxB5MGARSwm68fgIVt51o
=QwkD
-----END PGP SIGNATURE-----
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
There is nothing about Scala that makes it less suitable to this
problem than Haskell, except to the extent that Haskell enforces one
of the rules (no variables), but this difference is not related to the
specifics of this problem :) If you use Scala, you'll have to follow
this rule without any machine-checked proof that you have done so.
I am simply asking that you blindly follow this rule, rather than
discuss the merits of it.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1UU1MACgkQmnpgrYe6r61X2QCeJ3gsG1SFh9hQDQaZaFDV17kq
zPQAoML+nwpWP+BZES7/jedrZn0mObOU
=yRco
-----END PGP SIGNATURE-----
Ted Neward
Ted Neward
Java, .NET, XML Services
Consulting, Teaching, Speaking, Writing
http://www.tedneward.com
Andreas Scheinert
others that look for reference material to solve tonys problem:
http://jim-mcbeath.blogspot.com/2009/09/type-safe-builder-in-scala-part-4.html
This gives an example of how to construct a define a state machine
that counts, on the type level.
regards Andreas
On 11 Feb., 02:37, Ted Neward <t...@tedneward.com> wrote:
> +1
>
> Ted Neward
> Java, .NET, XML Services
Jim Powers
> others that look for reference material to solve tonys problem:http://jim-mcbeath.blogspot.com/2009/09/type-safe-builder-in-scala-pa...
> that counts, on the type level.
to work as advertised I certainly hope that something like this is not
part of the expected result. It certainly does not make a good
selling point about powerful static type systems enabling concision
and clarity in code. If I may offer my additional opinions ( ;-) )
all of that
> if (spec.length!=0) spec.length
> else spec.area/spec.width
stuff near the end seem aesthetically wrong to me, but hey, that's
me. Somehow it looks like Either should be used somewhere.
Andreas Scheinert
https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/ports/TicTacToe.scala
regards Andreas
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
This doesn't include the full solution. Specifically, it is missing
takeBack functionality.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1VpW8ACgkQmnpgrYe6r62vgwCdHsaEvVZb0UM58Mo5iCQDsaiI
GG0AnRgkCT6vfI7jnvUDMZmeTpJfFpiA
=MqQp
-----END PGP SIGNATURE-----
Raoul Duke
<andreas....@googlemail.com> wrote:
> SPOILER ALERT peak at your own risk at tonys solution:
> https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/ports/TicTacToe.scala
mapMOption isn't in scalaz?
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
(A => M[B]) => T[A] => M[T[B]]
...for implicit Monad[M] and Traverse[T]
Scalaz is not necessarily recommended for solving
this problem.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
OewAnRu8gmOI5kUa6o1BIAXjK0gs1MIZ
=ZF/m
-----END PGP SIGNATURE-----
Rex Kerr
--Rex
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Lack of clarity of the problem statement is certainly not what causes
difficulty.
>>
>>
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
3RIAn1QNRmg0CwVVGBkG57FgQkNrUkct
=t+Fb
-----END PGP SIGNATURE-----
Rex Kerr
trait MovableBoard {
def move[T <: Position](
board: BoardCanMakeMove[MovableBoard[T],T,MovedBoard],
position: T
): MovedBoard
}
where you require the client to pass in a "board" that not only declares that it can be moved to at a given position, but also contains the board with the move made. But now the client has tons of work to do to construct (or find) the appropriate board for the API.
But the exercise is still instructive, at least for pointing out the match between requirements of those sorts and language features that are not mysterious.
--Rex
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
On 12/02/11 08:15, Rex Kerr wrote:
> Well, one needs to use some judgment about what to do within the rules,
Yes.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1WOfAACgkQmnpgrYe6r60QLgCgmtJSqz1wjR1TcRLNIs98jO0S
LOAAoJ65TwH+O+nyXa4FfsrNbohvtJYU
=cGEh
-----END PGP SIGNATURE-----
Jim Powers
Thanks for sharing your solution. I will honestly admit that I have
only figured out about 40% of this (I thought I was further along, but
my solution wound up using implicit conversions meaning that the "type
errors" were discovered at run-time, not compile time :-( ). The
approach is definitely intriguing and useful for study.
--
Jim Powers
Rex Kerr
On reflection, Tony's make-the-user-pattern-match-my-custom-classes approach is probably the more elegant overall (though I'm not so sure about all of the other implementation details).
--Rex
HamsterofDeath
come up with somthing boring or something awesome.
:)
or nothing at all.
nicola...@gmail.com
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Thanks Nicholas.
On 13/02/11 22:04, nicola...@gmail.com wrote:
> A few side notes:
>
> - In a dependently typed language, like Agda, it would be possible
> to also check that a player only plays in an empty case.
Yes. One person is doing this, using Coq.
> (This can be done in Scala or Haskell too, but would rely on the
> fact that there is a known number of cases and would be quite heavy
> to do.)
I am doing this at this moment, using fundeps, for kicks. As far as I
know, there is no useful encoding of fundeps/MPTCs for Scala (anyone?).
> In such a language, you would not need to trust the library
> implantation, and the type would be more readable and informative.
> (as you use the same language to program at the level of values and
> the level of types.)
I am all for this dependent typing, but first we must teach
programmers what types even mean!
When I was lecturing a few years ago, I would encourage the head of
school to set an undergrad course on type theory. Various online
discussions inspired me, but those same discussions today make it
clear that I have lost. I have long since resigned.
>
> - If your students struggle with that exercise, I would suggest a
> slightly simpler one as a first exercise: Nim.
I agree though this risks the usual attraction of being too departed
from practical application. After all, it's just tic-tac-toe. I want
it to be hard enough that students recognise why you would encode an
API this way. Specifically, the *practical implications*.
>
> http://en.wikipedia.org/wiki/Nim
>
> You can start with a Nim game with one heap only. And have a few
> property to ensure at compile time:
>
> - game not finished - one move already done (for undoing) - one
> move already undone (for redoing) - player a turn (only when the
> game is not finished) - player b turn (idem)
>
> Maybe a simpler game would make it easier for your students to
> think about types.
Thanks for the tips mate. I'll keep trying!
>
>
> Best regards,
>
> Nicolas.
>
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1XyhgACgkQmnpgrYe6r60ENgCdH6FnVLbqH9JLSESO5WcLmRHT
hGoAoL5N8hZwM+crNP7+lNGDZe5qgnZw
=N5Ti
-----END PGP SIGNATURE-----
Jesper Nordenberg
> A few side notes:
>
> - In a dependently typed language, like Agda, it would be possible to
> also check that a player only plays in an empty case.
> (This can be done in Scala or Haskell too, but would rely on the fact
> that there is a known number of cases and would be quite heavy to do.)
I don't see why. You can encode the entire game logic in Scala's type
system and play the game at compile time.
/Jesper Nordenberg
Jim Powers
You can do user IO at compile time?
--
Jim Powers
HamsterofDeath
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
the programmer IS the player ;), and "compile" is "check my move"
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.14 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iQIcBAEBAgAGBQJNWX9vAAoJEFrE+uxgBUGAcC0QAIk7A47wplAXveKg8/BuS2aF
hiCa/lshfAAM8d+oCi6Y05lpwzRdkTU//my9d+B3sfJBLR0s24kGYz9XEYpDBOyZ
0obvGPDt6QkvCLCTwQLKieQzw+/3VzPlIBOiBspWKS/Ol+tWNNwgM5FUx85Q2BLb
4AHo5dYutXyhGRGEAWk29CeSTtvtW9DnyjnEO9T1lf2/L8pKXc/qJ+gErec0jrm4
nt+O0wG2b8ItYNNJ1kqg2End3w93OwHwqD12V1Zhth3gI3iG3BBnFnnNkSERxNdQ
/P7F8azIncnlNkgNwoLO7X69kGZwOn5nw11o7jbgi6wcMWsJQaH1wsb65sUh6719
FkP9Pavar75CyUEI0IghotPOqUtRwZX8MqghmZ6kQswP1W0SBkNbcKrGi4SLpd23
fW9OgTYlp1beiPGf9n+2lX1oaXU4cfQZXhrFtsuPSr/cD1C4E7Re+6Jg/UWaVyb5
qOvfIDTnNAFv/CfW1Yw+3+MAPXAaHC9pvdOr5cqLFzwwMD6xM3s2OQO6l70mYw7j
/5YORROBVSCtBS0Y1Ix+Zuf4deOWpNI5up03Qjwr4wsLaptHJbUygenW692iGSY4
4U9DI1jlNCzycmHmnt4Ha3nkzlLLMQBJ/2ko6hMzNgItqQK/XQwoHexB7e62P28V
TyLOhWi83UQtCsnihREt
=i4xF
-----END PGP SIGNATURE-----
Josh Suereth
Jim Powers
> Hash: SHA1
>
> Am 14.02.2011 20:13, schrieb Jim Powers:
>> On Mon, Feb 14, 2011 at 1:18 PM, Jesper Nordenberg
> <mega...@yahoo.com> wrote:
>>> nicola...@gmail.com skrev 2011-02-13 13:04:
>>>>
>>>> A few side notes:
>>>>
>>>> - In a dependently typed language, like Agda, it would be possible to
>>>> also check that a player only plays in an empty case.
>>>> (This can be done in Scala or Haskell too, but would rely on the fact
>>>> that there is a known number of cases and would be quite heavy to do.)
>>>
>>> I don't see why. You can encode the entire game logic in Scala's type
> system
>>> and play the game at compile time.
>>
>> You can do user IO at compile time?
>>
>
> the programmer IS the player ;), and "compile" is "check my move"
Yeah, but I would guess that this would not constitute a "typical"
user interaction model. Then again it would "teach" a lot of users a
bit about Scala programming indirectly ;-P.
>
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v2.0.14 (MingW32)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
>
> iQIcBAEBAgAGBQJNWX9vAAoJEFrE+uxgBUGAcC0QAIk7A47wplAXveKg8/BuS2aF
> hiCa/lshfAAM8d+oCi6Y05lpwzRdkTU//my9d+B3sfJBLR0s24kGYz9XEYpDBOyZ
> 0obvGPDt6QkvCLCTwQLKieQzw+/3VzPlIBOiBspWKS/Ol+tWNNwgM5FUx85Q2BLb
> 4AHo5dYutXyhGRGEAWk29CeSTtvtW9DnyjnEO9T1lf2/L8pKXc/qJ+gErec0jrm4
> nt+O0wG2b8ItYNNJ1kqg2End3w93OwHwqD12V1Zhth3gI3iG3BBnFnnNkSERxNdQ
> /P7F8azIncnlNkgNwoLO7X69kGZwOn5nw11o7jbgi6wcMWsJQaH1wsb65sUh6719
> FkP9Pavar75CyUEI0IghotPOqUtRwZX8MqghmZ6kQswP1W0SBkNbcKrGi4SLpd23
> fW9OgTYlp1beiPGf9n+2lX1oaXU4cfQZXhrFtsuPSr/cD1C4E7Re+6Jg/UWaVyb5
> qOvfIDTnNAFv/CfW1Yw+3+MAPXAaHC9pvdOr5cqLFzwwMD6xM3s2OQO6l70mYw7j
> /5YORROBVSCtBS0Y1Ix+Zuf4deOWpNI5up03Qjwr4wsLaptHJbUygenW692iGSY4
> 4U9DI1jlNCzycmHmnt4Ha3nkzlLLMQBJ/2ko6hMzNgItqQK/XQwoHexB7e62P28V
> TyLOhWi83UQtCsnihREt
> =i4xF
> -----END PGP SIGNATURE-----
>
>
--
Jim Powers
Jesper Nordenberg
If you rely on information not available at compile time (like user
input), it can never be completely type safe anyway. I'm just stating
that can Scala can be as type safe as any dependently typed language for
this type of problem.
/Jesper Nordenberg
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
be a compile-time error.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
dqgAniMASfqK5V+oWQVIP+7jtqGfWEfm
=rbS3
-----END PGP SIGNATURE-----
Jesper Nordenberg
> Jim Powers skrev 2011-02-14 20:13:
>> On Mon, Feb 14, 2011 at 1:18 PM, Jesper
>> Nordenberg<mega...@yahoo.com> wrote:
>>> nicola...@gmail.com skrev 2011-02-13 13:04:
>>>>
>>>> A few side notes:
>>>>
>>>> - In a dependently typed language, like Agda, it would be possible to
>>>> also check that a player only plays in an empty case.
>>>> (This can be done in Scala or Haskell too, but would rely on the fact
>>>> that there is a known number of cases and would be quite heavy to do.)
>>>
>>> I don't see why. You can encode the entire game logic in Scala's type
>>> system
>>> and play the game at compile time.
>>
>> You can do user IO at compile time?
>
> If you rely on information not available at compile time (like user
> input), it can never be completely type safe anyway.
Scratch "type safe". Obviously the more type information the compiler
has the more it can check at compile time. Encoding a move as a unique
type is only useful if the moves are available at compile time. If the
moves are inputted at runtime, a unique runtime representation is
sufficient.
/Jesper Nordenberg
Jim Powers
No. My confusion (if it is confusion) is if you "play" a game at
compile time (with a real user, not simply an algorithm walking
through all possible games) one would think that the compiler would
"stop" and "ask for input" from the user and then continue.
Resulting, in the end, of one game compiled and checked. This sound
intriguing, but kinda on the crazy-side to me. Either that or I'm
missing something fundamental.
Alternatively, folks could be talking about some tic-tac-toe version
of https://gist.github.com/66925, but the tower of hanoi is a
one-player game with a well-defined outcome (within the variation of
which pole gets the final move).
--
Jim Powers
Jesper Nordenberg
> No. My confusion (if it is confusion) is if you "play" a game at
> compile time (with a real user, not simply an algorithm walking
> through all possible games) one would think that the compiler would
> "stop" and "ask for input" from the user and then continue.
> Resulting, in the end, of one game compiled and checked. This sound
> intriguing, but kinda on the crazy-side to me. Either that or I'm
> missing something fundamental.
It can be done in the REPL I think. Each board state and move would be
represented with a unique type and you would have a function "def
doMove[M <: Move, B1 <: BoardState, B2 <: BoardState](move : M, board :
B1)(implicit mover : Mover[M, B1, B2]) : B2 = mover(move, board)". The
user can then interactively play a game by inputting the last return
value into the next doMove invokation.
/Jesper Nordenberg
Jim Powers
That I get. That's how I was "playing" my game in the version I was developing. But that's not really "at compile time" that's at "REPL" time (or the equivilent) for me "at compile time" is what happens you compile a c++ or Lisp file - a fully expressed piece of programming logic is translated into an "executable" form (for some appropriate definition of executable). Poking around in a REPL "interactively" is not expressing a complete body of programming logic, instead it just is, well, incrementally poking around. That's what a REPL is for: snippets of program code get evaluated in some environmental context and us shown to either be consistent or not consistent with that enironment.
OK granted one could replace the input loop in one of the solutions posted to the list with an input loop expecting snippets of code to be compiled and loaded (like the REPL) but that solution comes across as a tangent to the original problem. In the end I'm pretty damn confident it can be done, other than the fun of it I don't know why.
Jesper Nordenberg
> > It can be done in the REPL I think. Each board state and move would
> be represented with a unique type and you would have a function "def
> doMove[M <: Move, B1 <: BoardState, B2 <: BoardState](move : M, board :
> B1)(implicit mover : Mover[M, B1, B2]) : B2 = mover(move, board)". The
> user can then interactively play a game by inputting the last return
> value into the next doMove invokation.
>
> That I get. That's how I was "playing" my game in the version I was
> developing. But that's not really "at compile time" that's at "REPL"
> time (or the equivilent) for me "at compile time" is what happens you
> compile a c++ or Lisp file - a fully expressed piece of programming
> logic is translated into an "executable" form (for some appropriate
> definition of executable).
Sure it's done at compile time. All moves would be performed by the type
checker as it compiles the next REPL statement, and the actual running
of the generated code would be irrelevant. The return type is all that's
important.
Of course, you could just as well do the movement checking in runtime
and it would hardly be any difference to the player. But the idea of
evaluating a game at compile time is interesting IMHO.
/Jesper Nordenberg
Jim Powers
OK then. But you can absolutely play Tony's version in the REPL. The
input loop can be avoided altogether. The toString functions will
represent new board states in a "human readable" manner, but that's
not particularly important. I spent some time exploring Tony's
solution that way to convince myself that he had met his initial
specifications (to my satisfaction he did). All you have to do is
feed his functions the objects they want (of the proper type of course
;-) ) and have at it.
--
Jim Powers
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
FWIW, here is the game loop in Haskell. I also have similar in Scala.
https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/haskell/Data/TicTacToe/Interact.hs
Note that this is the single IO loop. The rest of the code lacks vriables.
It is entirely possible to play a game of tic-tac-toe without IO. More
to the point, there is nothing about tic-tac-toe that makes IO more or
less necessary than towers-of-hanoi. Doing this successfully is part
of the exercise. After all, the tests will have to generate games,
including complete ones.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aP0gACgkQmnpgrYe6r62TdgCgqjfQHXFtfgA9pKWhcOr7drbI
M+wAni9FZ3ggeLz1FDSgY1iQoi9Mi9MX
=8VB8
-----END PGP SIGNATURE-----
Kevin Wright
--
Kevin Wright
gtalk / msn : kev.lee...@gmail.com
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
>> let myMove = NW --> empty :type myMove
myMove :: Board
Your move.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aQfQACgkQmnpgrYe6r61WsgCdEzr/8DgEfFSG820miVnJtFlj
fRsAn1gmqVoB6cOR1k4PogNhL5topfJK
=pnhI
-----END PGP SIGNATURE-----
Kevin Wright
Kevin Wright
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
It does, but it's not necessary to play.
NW --> empty
Your move.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aQvgACgkQmnpgrYe6r61lkgCeJCt7/KWj87DNfetVz5WY6tsE
1jwAnRuneJdDrxDR8EPt6iMRAj8oTDKx
=f3YK
-----END PGP SIGNATURE-----
Kevin Wright
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Shall we use a dependently-typed language then? Or, does your belief
that IO is necessary require a specific representation of the program,
specifically, a representation requiring IO?
Let us assume, for the sake of emphasis that I is unnecesary, that the
value returned has this type:
BoadWithASingleMoveMadeAtNW
Your move.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aRVcACgkQmnpgrYe6r62DAwCgjLKwaxaCHuBYZnQkRyBpNg09
srEAoMkaS6ioKLIuBUOIhI1v7MDroD2L
=dSi5
-----END PGP SIGNATURE-----
Kevin Wright
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
I'll upload the answer to these questions to hackage for you. Stay tuned.
>
> Without IO the returned value only exists in isolation, within the
> compiler.
WTF?
> It's not something that I as a player can use, just something the
> compiler can use.
Wibbly Wobbly WTF?
>
> If course, I can have *already* entered my follow-up move which the
> compiler will also dutifully assign to a return type, but how did I
> know what move to make?
Just to clarify, how did you know what move to make? You choose one of
8 possibilities. That's an essential part of the game.
If you're not sure which 8 are available to you or what state the
board is in, please revisit the type. While you're visiting, note the
absence of IO.
>
> I either spoke to you and we agreed in advance what moves we would
> type in, or we took turns editing source code. *this* is when the
> true "playing" of the game actually took place, and it involved IO
> (either human-human or human-computer). Once scalac or ghc (or
> whatever) is invoked the actual game is already past tense, the
> compiler is simply validating and encoding the pre-existing game
> into some other format.
>
You are making a distinction that doesn't exist. This is the extremely
important, single point of this exercise -- to break this idea.
Again, your move.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aSQwACgkQmnpgrYe6r61NuQCdHqffbQw7SnyG7SBFHYDvPe+E
yu4An166MMC93zS+1xWXH6nwttPC8RI2
=sG1i
-----END PGP SIGNATURE-----
Kevin Wright
>You are making a distinction that doesn't exist. This is the extremely
> I either spoke to you and we agreed in advance what moves we would
> type in, or we took turns editing source code. *this* is when the
> true "playing" of the game actually took place, and it involved IO
> (either human-human or human-computer). Once scalac or ghc (or
> whatever) is invoked the actual game is already past tense, the
> compiler is simply validating and encoding the pre-existing game
> into some other format.
>
important, single point of this exercise -- to break this idea.
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
> It's not always 8 possibilities,
Yes it is. Please see the type. You have 8 possibilities, one of which
is not NW. Anything else *will not compile*.
Your move.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aTWcACgkQmnpgrYe6r62vpwCgnZgQsrGq2dnoRsp+aZjbnEZk
IjMAoKxxnOYFXWc5cP/f3ruftuy7KV7/
=pJ/B
-----END PGP SIGNATURE-----
Artem Khodyush
The point is, you can't see *anything* without 'it' going through some
kind of IO somewhere (unless you are claiming solipsism, in which case
there is no need to discuss anything anyway :-)
Kevin Wright
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
> It's not always 8 possibilities,Yes it is. Please see the type. You have 8 possibilities, one of which
is not NW. Anything else *will not compile*.
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Are you suggesting you need IO in order to come to know the type?
If that's the case, we have even bigger problems.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aUQoACgkQmnpgrYe6r62rBgCcCyHi+gClOliN4h4NjggPiyq7
I6AAn2YjQZEYPDqAQTvoHwQQ/4HN20qZ
=ctPJ
-----END PGP SIGNATURE-----
Kevin Wright
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Are you suggesting you need IO in order to come to know the type?On 15/02/11 20:02, Kevin Wright wrote:
> On 15 February 2011 09:54, Tony Morris <tonym...@gmail.com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>>
>>> It's not always 8 possibilities,
>> Yes it is. Please see the type. You have 8 possibilities, one of
>> which is not NW. Anything else *will not compile*.
>>
>>
> But how did I know that?
>
> I either read the type after it was output to me, or I read the
> code that you input and determined what the type would be. Either
> way... IO is involved wherever I need interaction. I can drop the
> IO only if I drop the interaction, but once I do that I'm no longer
> "playing" a game.
>
If that's the case, we have even bigger problems.
nicola...@gmail.com
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
We seem to have departed from what I meant by IO.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aU5oACgkQmnpgrYe6r60BbACdHgu1LLrY9nYvNMLOVHfHaBvz
ZKUAoJ7rBuJ64W+A6VDC59ZFYlUSPBro
=Ohc/
-----END PGP SIGNATURE-----
Kevin Wright
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
We certainly can play a game without IO. You just refused to make your
move :)
On a more serious note, I deliberately meant "play" in that way,
because it is important to observe that the essence of what it means
to play is explicitly distinct from anything resembling IO. It s not a
necessary component of playing. It is, only in so far as you decide to
represent your program that way -- it not some inherent property of play.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aVPMACgkQmnpgrYe6r60/DQCfQ6zV2cUbd257LkMFalCYBVvl
vVYAoIZz2cnfaUcLbRU7xosOCjgL6PQC
=LQME
-----END PGP SIGNATURE-----
Kevin Wright
On a more serious note, I deliberately meant "play" in that way,
because it is important to observe that the essence of what it means
to play is explicitly distinct from anything resembling IO. It's not a
necessary component of playing. It is, only in so far as you decide to
represent your program that way -- it not some inherent property of play.
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
No, it's not the nature. It's how you decided to represent playing.
The exercise is to encourage you to represent it by other means, to
depart from any notion of inherent IO to the solution, since it is not
required.
I assure you, it's possible to play a game without IO. Depdendent
typing and hypothesising aside, the tests do exactly that. You can
look at them for yourself. They exist, they play a game, they do not
use IO, because if they did, *the program would not compile*.
Let me be explicit. I can write a function that quantifies on all
possible played games. I needn't resort to IO to do this. I have done
this. You can see it.
I think it's also clear that I am using a very distinct definition for
IO, where you are using something loose.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aV7AACgkQmnpgrYe6r60IlwCeJbblemUjpVgzKb43Ymhvs5zl
ihkAoMp2MiKWKnkxwCm8XpbbUiGu7xEq
=W1Ng
-----END PGP SIGNATURE-----
Steven Obua
If you are seriously interested in the nature of games like "Nim", check out Conways "On numbers and games". Can be understood without any reference to types.
- Steven Obua
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
I am high on painkillers at the moment. I shall assume this was a
joke. I hope this is OK with you.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1aWTAACgkQmnpgrYe6r62pvQCeP1zUovVl7vsTj906rZslfUzy
qDAAmgIrn/IJ62cq+I1TgqJCt2SQYMft
=xKjq
-----END PGP SIGNATURE-----
Johannes Rudolph
<steve...@googlemail.com> wrote:
> It seems to me that one of the serious drawbacks of static typing has manifested itself: much ado about nothing ;-)
Oh no, please don't do this and stop this enlightening and very
entertaining discussion. I was expecting this discussion to quickly
move forward to other serious and important topics like philosophy
(determinism, what are decisions, what is a game without decisions,
the free will, generally), sports (how can a referee interfere without
IO), esotherics (is telepathy IO? and what about telekinetics),
quantum physics (how to describe the type of a game simultaneously
played in all parallel realities), staged computing (where to put the
line between compile time and run time, should that itself be decided
at compile time or run time or even before?), the future of the scala
compiler (what are the chances of it taking part in creating the
singularity, and will the type of the singularity still be a supertype
of Nothing?) etc. I expected serious results in the next few hours. I
hope you didn't spoil that.
--
Johannes
-----------------------------------------------
Johannes Rudolph
http://virtual-void.net
Jim Powers
HA! Yes, it does seem to be destined to do that, yes. There must be
an analogy to Godwin's Law for this kind of thing.
I think the challenge is simple: produce a program that plays
tic-tac-tow with no IO at all (either directly or indirectly) that any
pair of human beings can play. By "play" I'm expressing the commonly
accepted notion that the human beings in question can express their
choice during their turn through the program to the other player.
Continuing in this fashion until the game is finished.
"Playing" tic-tac-tow through test cases either exactly expresses
proof by exhaustive search or approximates it. If one could prove
Tony's code (or any code for that matter, perhaps even using ATS
embedding the proof in the code) correct why even bother with the test
cases? Not only would IO be irrelevant, but even "playing" computer
or otherwise, would be irrelevant (I'm talking about the tic-tac-toe
game, not arbitrary code where correctness proofs are invaluable). As
far as conscious creatures are concerned computations are only
interesting if artifacts of such computations can enter the minds of
conscious creatures. Other than that it's a bunch of computations
over forever hidden variables burning up the limit free energy in the
cosmos.
--
Jim Powers
Razvan Cojocaru
Kevin Wright
Kevin Wright
gtalk / msn : kev.lee...@gmail.com
Francois
> On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
> "Playing" tic-tac-tow through test cases either exactly expresses
> far as conscious creatures are concerned computations are only
> interesting if artifacts of such computations can enter the minds of
> conscious creatures. Other than that it's a bunch of computations
> over forever hidden variables burning up the limit free energy in the
> cosmos.
Well, minus the fact that you loose the goal of the topic: make people
be better with type management, encoding of only possible states, and
things like that.
That being said... Thanks Tony for the proposed subject, it was
entairtaining to code it and make be better with what works OK with
Scala types - and with the fact that the type safeness of API matters,
internal state may not be as type safe, as long as it remove code
duplication and make the whole thing cleaner (for example because Scala
does not have full dependant-type support).
Thanks,
--
Francois ARMAND
http://fanf42.blogspot.com
http://www.normation.com
Derek Williams
> It'll be Schrödinger's tic-tac-toe. The game has maybe been played, or it
> hasn't, and any winner is indeterminate until IO collapses the type
> hierarchy...
> I wonder what's happening with that quantum type system that the Java Posse
> predicted?
This whole thread sounds like a (educated) version of the drunk
discussions I've had with my friends regarding reality, our perception
of reality, and if we can actually know if it exists or not, and if
that really matters.
Or like an assembly class I was in, where we had to create a simple
calculator. Apparently the point of the project was to teach us about
overflow. I made it impossible for mine to overflow (it wouldn't
accept your keypress if the result would overflow), and the teacher
said I missed the point and made me redo it. Wonderful teaching there.
Thanks.
To bring this back on subject (kind of), you don't need to decide a
next move. Just follow this: http://xkcd.com/832/
--
Derek
Jim Powers
Completely agreed. The problem and the few solutions that have been
posted have got me very excited. I'm in the process of applying some
of the techniques to code I'm working on with some nice results --
thanks Tony.
I guess perhaps it was a lost-in-translation thing, but the notion of
pushing back the "play" of the game into the compiler seemed besides
the point. It appeared that the point was to use types in a more
comprehensive and constructive manner - use types as a tool to better
express how the program maps to the problem domain. I will admit that
I do tend to slide into "Scala as a better Java" state of mind when I
should know better. Tony's problem and example code was a needed kick
in the arse.
--
Jim Powers
Tony Morris
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
I honestly didn't expect the fuss or appeals to mysticism.
Nevertheless, I hope the important point was learned.
- --
Tony Morris
http://tmorris.net/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk1a65EACgkQmnpgrYe6r6271QCfT4rsoynXp7mpU+lI5a9jKh9l
whYAoL8uDH8B4jsWoE8LF6hz5l4f1XQL
=sKWi
-----END PGP SIGNATURE-----
Jim Balter
-- Jim
Artem Khodyush
encode state, so that "illegal state exception" becomes compile-time
error, right?
If so, can someone point to more examples of this kind, perhaps more
'pragmatic' or close to real-life code? IO definitely comes to mind -
I remember seeing somewhere how one can use different types for
representing open and closed file descriptor, so you can never do IO
on closed files - but I can't find the link now.
Another example is 'type-safe builder pattern' described in
http://blog.rafaelferreira.net/2008/07/type-safe-builder-pattern-in-scala.html
Are there anything else?
--
Thanks,
Artem
Tony Morris
> So, the point of this exercise is to teach people how to use types to
> encode state, so that "illegal state exception" becomes compile-time
> error, right?
ultimately unusable.
By unnecessary IO, you are encouraged to choose different techniques to
observe the fact e.g. Haskell where any IO is encoded in the type (and
so the machine will force you to own up) or Scala where you simply trust
your own judgment -- however too often I see an over-estimate here so I
recommend this with apprehension.
> If so, can someone point to more examples of this kind, perhaps more
> 'pragmatic' or close to real-life code? IO definitely comes to mind -
> I remember seeing somewhere how one can use different types for
> representing open and closed file descriptor, so you can never do IO
> on closed files - but I can't find the link now.
>
> Another example is 'type-safe builder pattern' described in
> http://blog.rafaelferreira.net/2008/07/type-safe-builder-pattern-in-scala.html
>
> Are there anything else?
>
There is nothing particularly special about this style of programming.
It is true that messier designs and poorly written APIs are very
popular. The goal of the exercise is to advance your API design skills
so that what might look foreign at the moment, becomes the default mode
of problem solving. I believe some commentators call it discipline or
zen or something like that. I just call it practical software development.
Good luck!
Tony Morris
> I'll upload the answer to these questions to hackage for you. Stay tuned.
http://hackage.haskell.org/package/TicTacToe
Note a complete API, permitting game play, without the use of variables
(IO type constructor).
http://hackage.haskell.org/packages/archive/TicTacToe/latest/doc/html/Data-TicTacToe-Board.html
I can also send the scaladoc, however, the types do not enforce a lack
of variables, so it's not as obvious.
Stefan Wagner
> ...
> Write an API for tic-tac-toe.
I wrote an API for Tic-Tac-Toe, and a game which uses the API. The api
does no IO, but the game does. And I followed - mostly - the
instructions from your website, which is unavailable right now.
The problem there is slightly different from the tic-tac-toe here, but I
will try this one here, too.
In one point I didn't understand the task: the method 'move' should take
a status and a pos, and return a data structure. I had no idea what
'status' should be used for, and expected to find out while solving the
task, but then I was done without it. So it's just a placeholder.
But when I read here about church-numerals and so on, I guess I choosed
a too simple solution and didn't get the question right.
Here is my approach. (Attached to preserve indentation).
// just two, dumb players:
sealed abstract class Player
object O extends Player { override def toString () = "O" }
object X extends Player { override def toString () = "X" }
/* Positions (x,y) (col,row):
(1,1)|(2,1)|(3,1)
----------------
(1,2)| | O
----------------
(1,3)| X |
*/
final class Position (val x: Int, val y: Int) {
override def toString () = "(" + x + ", " + y + ")"
// we don't override hashcode, because we're lazy, and: YAGNI
override def equals (other: Any) = other match {
case o: Position => x == o.x && y == o.y
case _ => false
}
}
abstract sealed class Game (val xPos : List [Position], val oPos : List
[Position]) {
/**
find triple in row, in col, in falling or climbing diagonal
*/
def triple (pl : List[Position]) : Boolean = {
val n = List (1, 2, 3)
val xs = (for (i <- n) yield ((pl.filter (_.x == i)).length ==
3)).exists (_ == true)
val ys = (for (i <- n) yield ((pl.filter (_.y == i)).length ==
3)).exists (_ == true)
val diag1 = (pl.filter (e => e.x == e.y).length == 3)
/** a little math:
4x diag2: y = 4 - x
3| x
2| x
1| x
0|-------X
0 1 2 3 4
*/
val diag2 = (pl.filter (e => 4 - e.x == e.y).length == 3)
xs || ys || diag1 || diag2
}
def playerAt (pos: Position) : Option[Player] = {
if (oPos.contains (pos)) Some (O) else
if (xPos.contains (pos)) Some (X) else
None
}
}
class RunningGame (xPos: List[Position] = List (), oPos: List[Position]
= List ()) extends Game (xPos, oPos) {
// why status? just to fulfill the contract :)
def move (status: String, pos: Position) : Game = {
val player = whosTurn ()
val nPos = if (player == X)
pos :: xPos else
pos :: oPos
// println (player + ": " + nPos)
// one player won or player one made 4 steps and is now doing step 5
if (triple (nPos) || xPos.length == 4 && player == X)
player match {
case X => new CompletedGame (nPos, oPos)
case O => new CompletedGame (xPos, nPos)
} else
player match {
case X => new RunningGame (nPos, oPos)
case O => new RunningGame (xPos, nPos)
}
}
// by our convention, games start always with X
def whosTurn () : Player = if (oPos.length == xPos.length) X else O
}
class CompletedGame (xl: List[Position], ol: List[Position]) extends
Game (xl, ol) {
def whoWon () : Option[Player] = {
if (triple (xPos)) Some (X) else
if (triple (oPos)) Some (O) else
None
}
}
/**
Testprogram with output and random input:
*/
object TicTacToe {
// additional method for viewing
def show (g: Game) = {
for (row <- (1 to 3);
col <- (1 to 3)) {
val p = g.playerAt (new Position (col, row))
if (p == Some (X)) print (" X " )
else if (p == Some (O)) print (" O ")
else print (" . ")
if (col == 3) println ()
}
println ()
}
/**
call step recursively
*/
def step (rnd : util.Random, game : RunningGame) : Unit = {
val x = rnd.nextInt (3) + 1
val y = rnd.nextInt (3) + 1
val pos = new Position (x, y)
if (game.playerAt (pos) == None) {
// println ("No player at x,y = " + pos)
val g = game.move ("foo", pos)
show (g)
g match {
case rg: RunningGame => step (rnd, rg)
case cg: CompletedGame => {
println ("Complete! Winner: " + cg.whoWon ())
()
}
}
} else
{
// println ("surprise! player at x,y " + pos + " = " +
game.playerAt (pos))
step (rnd, game)
}
}
/**
Initialize random generator
val winner
--- ------
17 X in last step
23 X early
42 O
9 None
*/
def main (args : Array [String]) : Unit = {
val rnd = new util.Random (args(0).toLong)
val game = new RunningGame ()
step (rnd, game)
}
}
--
Tschööö--->...Stefan
---------------------------
Don't visit my homepage at:
http://home.arcor-online.net/hirnstrom
Tony Morris
Congrats on making it that far on the exercise. I know it can be
difficult. I have provided some critique below. I hope you don't mind.
On 17/02/11 10:20, Stefan Wagner wrote:
> Tony Morris schrieb:
>> ...
>> Write an API for tic-tac-toe.
> I wrote an API for Tic-Tac-Toe, and a game which uses the API. The api
> does no IO, but the game does. And I followed - mostly - the
> instructions from your website, which is unavailable right now.
>
> The problem there is slightly different from the tic-tac-toe here, but I
> will try this one here, too.
>
> In one point I didn't understand the task: the method 'move' should take
> a status and a pos, and return a data structure. I had no idea what
> 'status' should be used for, and expected to find out while solving the
> task, but then I was done without it. So it's just a placeholder.
I'm not sure why you think it should accept a status. Did I say that? If
so, I do not recall and I'm sorry for misleading.
> But when I read here about church-numerals and so on, I guess I choosed
> a too simple solution and didn't get the question right.
>
> Here is my approach. (Attached to preserve indentation).
>
> // just two, dumb players:
> sealed abstract class Player
> object O extends Player { override def toString () = "O" }
> object X extends Player { override def toString () = "X" }
I don't think you need to override toString if you make these case
objects. Note that this data type is isomorphic to Boolean.
> /* Positions (x,y) (col,row):
> (1,1)|(2,1)|(3,1)
> ----------------
> (1,2)| | O
> ----------------
> (1,3)| X |
> */
> final class Position (val x: Int, val y: Int) {
This means that there are 2^64 possible positions. What happens when I,
as a client of your API, construct a Position with say 25363 and 5673452?
I think you should disallow "undefinedness" with the type system. There
are exactly nine possible positions. You can represent this with your
own data type and nullary constructors (case objects).
> override def toString () = "(" + x + ", " + y + ")"
> // we don't override hashcode, because we're lazy, and: YAGNI
> override def equals (other: Any) = other match {
> case o: Position => x == o.x && y == o.y
> case _ => false
> }
I think you'll get this automatically with a case class/object, but your
toString would be a little different.
> }
>
> abstract sealed class Game (val xPos : List [Position], val oPos : List
> [Position]) {
This constructor has a similar problem to position. As a client of the
API, I am able to create a Game in an inconsistent state. There are many
ways to do this:
* I could have the lengths of xPos and yPos be considerably different,
meaning one player has played out of order.
* I could have Lists with a length of more than is available on the board.
* I could have a List containing duplicate positions.
All of these are able to be avoided with type-safety and easily with
Scala (even Java for that matter). I encourage you to try it. I'm happy
to provide hints here if you like.
You might say that you are solving a more general problem of a n-by-n
board, rather than 3-by-3. This would change the enforced invariants,
but you could still enforce a lot more than is current.
--
Tony Morris
http://tmorris.net/
Stefan Wagner
Hash: SHA1
Hi Tony, Hi List,
> Hi Stefan,
> Congrats on making it that far on the exercise. I know it can be
> difficult. I have provided some critique below. I hope you don't mind.
I'm happy, because I did it for the critique.
>> The problem there is slightly different from the tic-tac-toe here, but I
>> will try this one here, too.
>>
>> In one point I didn't understand the task: the method 'move' should take
>> a status and a pos, and return a data structure. I had no idea what
>> 'status' should be used for, and expected to find out while solving the
>> task, but then I was done without it. So it's just a placeholder.
> I'm not sure why you think it should accept a status. Did I say that? If
> so, I do not recall and I'm sorry for misleading.
The website is reachable again.
" The move function will take a game state, a Position and it will
return a data type that you write yourself." But if you're fine with
dropping a state-val, so am I.
>> object X extends Player { override def toString () = "X" }
> I don't think you need to override toString if you make these case
> objects. Note that this data type is isomorphic to Boolean.
In the grid, it works fine without toString, but the winner-message is
not that clean now:
X O X
X X O
O O X
Complete! Winner: Some(X$@18fb1f7)
I'm not ready with your suggestions and critique, but partly so, but
since I encountered a phenomen, I want to mention, which might vanish in
the remaining process, I like to mention it right now.
>> final class Position (val x: Int, val y: Int) {
> This means that there are 2^64 possible positions. What happens when I,
> as a client of your API, construct a Position with say 25363 and 5673452?
The client of the API is always some kind of IO-Monad in critique state.
:) I managed to get rid of the ints with some final sealed objects:
// Orientation itself isn't used right now, but for completeness...
sealed abstract class Orientation
sealed abstract class Vertical extends Orientation
sealed abstract class Horizontal extends Orientation
object NORTH extends Vertical
object CENTER extends Vertical
object SOUTH extends Vertical
object WEST extends Horizontal
object MIDDLE extends Horizontal
object EAST extends Horizontal
final class Position (val h: Horizontal, val v: Vertical) {
val x = h match {
case WEST => 1
case MIDDLE => 2
case EAST => 3
}
val y = v match {
case NORTH => 1
case CENTER => 2
case SOUTH => 3
}
// we don't override hashcode, because we're lazy, and: YAGNI
override def equals (other: Any) = other match {
case o: Position => x == o.x && y == o.y
case _ => false
}
}
// Of course I have to modify the game accordingly.
/**
Testprogram with Output and Random-Input:
*/
object TicTacToe {
val horizontals = List (WEST, MIDDLE, EAST)
val verticals = List (NORTH, CENTER, SOUTH)
// additional method for viewing
def show (g: Game) = {
for (row <- horizontal
col <- verticals) {
val p = g.playerAt (new Position (row, col))
if (p == Some (X)) print (" X " )
else if (p == Some (O)) print (" O ")
else print (" . ")
if (col == SOUTH) println ()
}
println ()
}
Here I had an error. I tested in the 4th line from bottom:
if (col == 3) println ()
as before, and didn't get a compile error, but ...
scala TicTacToe 17
X . . . . . . . .
X . . . . O . . .
X . . X . O . . .
X . . X . O O . .
X . X X . O O . .
X O X X . O O . .
X O X X . O O . X
X O X X . O O O X
X O X X X O O O X
Complete! Winner: Some(X$@18fb1f7)
...a nice graph. What? Didn't I went that way to improve type safety?
'col' is an Element of the List of verticals, and I thought it is
therefore inferred to be a vertical. Does the typer consider the whole
method, and searches for the common superclass of Vertical and 3? And
would only have warned me, if I made a call outside the method, to
another method? Okay, I can try to find it out by myself.
>> abstract sealed class Game (val xPos : List [Position], val oPos : List
>> [Position]) {
> This constructor has a similar problem to position. As a client of the
> API, I am able to create a Game in an inconsistent state. There are many
> ways to do this:
> * I could have the lengths of xPos and yPos be considerably different,
> meaning one player has played out of order.
> * I could have Lists with a length of more than is available on the board.
> * I could have a List containing duplicate positions.
That will take some more time. I come back to it later. First I have a
little work to do, shopping and dinner.
A part of the problem might vanish, if I am able to prohibit
modification of the Lists of positions. And I guess I'm already partly
there. The User doesn't put, oh well! he shouldn't put positions into
the List himself, but I add the new positions alternating to X's
positions or O's positions. Well, but I don't prevent the user from
doing fraud. ... I need definetively a few hours, to concentrate a
little on this. So long, and thank you for your advice. :)
- --
Tsch���--->...Stefan
- ---------------------------
Don't visit my homepage at:
http://home.arcor-online.net/hirnstrom
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iEYEARECAAYFAk1dWAMACgkQQeATqGpDnRpPYQCfV3ygXTPyFjJ2k7C1sSRXRNGu
OH0An3a7uUt/4bdj/UCs0P24gCZci++j
=cZTl
-----END PGP SIGNATURE-----
Stefan Wagner
Hash: SHA1
Hi Tony, Hi List,
to the question, why (col == 3) does compile:
Here is the output of
scalac -Xprint:typer TicTacToe.scala
def show(g: Game): Unit = {
Orientation.horizontals.foreach[Unit](((row: Horizontal) =>
Orientation.verticals.foreach[Unit](((col: Vertical) => {
val p: Option[Player] = g.playerAt(new Position(row, col));
if (p.==(scala.Some.apply[object X](X)))
scala.this.Predef.print(" X ")
else
if (p.==(scala.Some.apply[object O](O)))
scala.this.Predef.print(" O ")
else
scala.this.Predef.print(" . ");
if (col.==(3))
scala.this.Predef.println()
else
()
}))));
scala.this.Predef.println()
};
There in the loop-head is 'col: Vertical' recognized as expected, so I
would expect '(col == 3)' to be an compile time error.
- --
Tsch���--->...Stefan
- ---------------------------
Don't visit my homepage at:
http://home.arcor-online.net/hirnstrom
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iEUEARECAAYFAk1dXdcACgkQQeATqGpDnRpZ/gCfTIfwH0cpEybkw95NVDBGvsR9
4BQAl2xeZ0UOtzwBsP29U7CmPp0ifqI=
=Es6i
-----END PGP SIGNATURE-----
Andreas Scheinert
See Tony your efforts were not in vain, infact (some people) did the
practice and learned something. If pushing the limits of the compiler/
typesystem becomes more common this will lead eventually to
improvements:
http://groups.google.com/group/scala-user/t/2efabc7c1237c585
Regards andreas
> Don't visit my homepage at:http://home.arcor-online.net/hirnstrom
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.9 (GNU/Linux)