This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Re: Re: Benefits of static typing

32 replies
Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 12/02/11 07:20, Raoul Duke wrote:
> On Fri, Feb 11, 2011 at 1:08 PM, Andreas Scheinert
> andreas [dot] scheinert [at] googlemail [dot] com (<andreas [dot] scheinert [at] googlemail [dot] 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?

Yes and generalised of course.
(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/

iEYEARECAAYFAk1VqLAACgkQmnpgrYe6r61d/wCeM4Rgr60/aPwi+b3VTf0qJXge
OewAnRu8gmOI5kUa6o1BIAXjK0gs1MIZ
=ZF/m
-----END PGP SIGNATURE-----

Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 09:08, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:


On 15 February 2011 09:05, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:00, Kevin Wright wrote:
> On 15 February 2011 08:54, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 10:40, Jim Powers wrote:
>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper Nordenberg
>>> <megagurka [at] yahoo [dot] com> wrote:
>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>
>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>> <megagurka [at] yahoo [dot] com <mailto:megagurka [at] yahoo [dot] com>> wrote:
>>>>>> 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.
>>>
>>> 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.
>>>
>> 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/
>>
>>
> I'd argue that point... Sure you can "simulate" a game without IO,
> but "play" it?
>
>
>> let myMove = NW --> empty :type myMove
myMove :: Board

Your move.

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


The "read" of read-evaluate-print-loop most definitely counts as IO :)

as does the "print"
Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 09:10, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:09, Kevin Wright wrote:
> On 15 February 2011 09:08, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com>
> wrote:
>
>>
>>
>> On 15 February 2011 09:05, Tony Morris <tonymorris [at] gmail [dot] com>
>> wrote:
>>
>>>
>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>
>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>> On 15 February 2011 08:54, Tony Morris
>>>> <tonymorris [at] gmail [dot] com> wrote:
>>>>
>>>>>
>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>
>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper Nordenberg
>>>>>> <megagurka [at] yahoo [dot] com> wrote:
>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>
>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>> <megagurka [at] yahoo [dot] com <mailto:megagurka [at] yahoo [dot] com>>
>>>>>>>> wrote:
>>>>>>>>> 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.
>>>>>>
>>>>>> 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.
>>>>>>
>>>>> 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/
>>>>>
>>>>>
>>>> I'd argue that point... Sure you can "simulate" a game
>>>> without IO, but "play" it?
>>>>
>>>>
>>>>> let myMove = NW --> empty :type myMove
>>> myMove :: Board
>>>
>>> Your move.
>>>
>>> - -- Tony Morris http://tmorris.net/
>>>
>>>
>> The "read" of read-evaluate-print-loop most definitely counts as
>> IO :)
>>
>>
> as does the "print"
>
It does, but it's not necessary to play.

NW --> empty

Your move.


How should I enter it?  Or know what move you made?  Without inputing somewhere, or reading what you typed and has since been output to the console.
If it's not to be done via the repl then the whole thing must be compiled atomically, with no scope for interaction.  Without interaction, the act of compilation is not playing the game, it's merely simulating a game that we've already played outside of the compiler.
Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:16, Kevin Wright wrote:
> On 15 February 2011 09:10, Tony Morris
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 19:09, Kevin Wright wrote:
>>> On 15 February 2011 09:08, Kevin Wright
>>> wrote:
>>>
>>>>
>>>>
>>>> On 15 February 2011 09:05, Tony Morris
>>>> wrote:
>>>>
>>>>>
>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>
>>>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>>>> On 15 February 2011 08:54, Tony Morris
>>>>>> wrote:
>>>>>>
>>>>>>>
>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>
>>>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper Nordenberg
>>>>>>>> wrote:
>>>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>>>
>>>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>>>> >>>>>>>>> > wrote:
>>>>>>>>>>> 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.
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>
>>>>>>> FWIW, here is the game loop in Haskell. I also have
>>>>>>> similar in Scala.
>>>>>>>
>>>>>>>
>>>>>
>>>>>
>>
>>
https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/haskell/...
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>
>>>>>
>>
>>
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/
>>>>>>>
>>>>>>>
>>>>>> I'd argue that point... Sure you can "simulate" a game
>>>>>> without IO, but "play" it?
>>>>>>
>>>>>>
>>>>>>> let myMove = NW --> empty :type myMove
>>>>> myMove :: Board
>>>>>
>>>>> Your move.
>>>>>
>>>>> - -- Tony Morris http://tmorris.net/
>>>>>
>>>>>
>>>> The "read" of read-evaluate-print-loop most definitely counts
>>>> as IO :)
>>>>
>>>>
>>> as does the "print"
>>>
>> It does, but it's not necessary to play.
>>
>> NW --> empty
>>
>> Your move.
>>
>>
> How should I enter it? Or know what move you made? Without
> inputing somewhere, or reading what you typed and has since been
> output to the console.
>
> If it's not to be done via the repl then the whole thing must be
> compiled atomically, with no scope for interaction. Without
> interaction, the act of compilation is not playing the game, it's
> merely simulating a game that we've already played outside of the
> compiler.
>
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 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:09, Kevin Wright wrote:
> On 15 February 2011 09:08, Kevin Wright
> wrote:
>
>>
>>
>> On 15 February 2011 09:05, Tony Morris
>> wrote:
>>
>>>
>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>
>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>> On 15 February 2011 08:54, Tony Morris
>>>> wrote:
>>>>
>>>>>
>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>
>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper Nordenberg
>>>>>> wrote:
>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>
>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>> >
>>>>>>>> wrote:
>>>>>>>>> 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.
>>>>>>
>>>>>> 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.
>>>>>>
>>>>> FWIW, here is the game loop in Haskell. I also have similar
>>>>> in Scala.
>>>>>
>>>>>
>>>
>>>
https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/haskell/...
>>>>>
>>>>>
>>>>>
>>>
>>>
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/
>>>>>
>>>>>
>>>> I'd argue that point... Sure you can "simulate" a game
>>>> without IO, but "play" it?
>>>>
>>>>
>>>>> let myMove = NW --> empty :type myMove
>>> myMove :: Board
>>>
>>> Your move.
>>>
>>> - -- Tony Morris http://tmorris.net/
>>>
>>>
>> The "read" of read-evaluate-print-loop most definitely counts as
>> IO :)
>>
>>
> as does the "print"
>
It does, but it's not necessary to play.

NW --> empty

Your move.

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:28, Kevin Wright wrote:
> On 15 February 2011 09:20, Tony Morris
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 19:16, Kevin Wright wrote:
>>> On 15 February 2011 09:10, Tony Morris
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 19:09, Kevin Wright wrote:
>>>>> On 15 February 2011 09:08, Kevin Wright
>>>>> wrote:
>>>>>
>>>>>>
>>>>>>
>>>>>> On 15 February 2011 09:05, Tony Morris
>>>>>> wrote:
>>>>>>
>>>>>>>
>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>
>>>>>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>>>>>> On 15 February 2011 08:54, Tony Morris
>>>>>>>> wrote:
>>>>>>>>
>>>>>>>>>
>>>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>>>
>>>>>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper
>>>>>>>>>> Nordenberg wrote:
>>>>>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>>>>>
>>>>>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>>>>>> >>>>>>>>>>> > wrote:
>>>>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>> FWIW, here is the game loop in Haskell. I also
>>>>>>>>> have similar in Scala.
>>>>>>>>>
>>>>>>>>>
>>>>>>>
>>>>>>>
>>>>
>>>>
>>
>>
https://bitbucket.org/dibblego/haskell-course/src/tip/TicTacToe/haskell/...
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>
>>>>>>>
>>>>
>>>>
>>
>>
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/
>>>>>>>>>
>>>>>>>>>
>>>>>>>> I'd argue that point... Sure you can "simulate" a
>>>>>>>> game without IO, but "play" it?
>>>>>>>>
>>>>>>>>
>>>>>>>>> let myMove = NW --> empty :type myMove
>>>>>>> myMove :: Board
>>>>>>>
>>>>>>> Your move.
>>>>>>>
>>>>>>> - -- Tony Morris http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>> The "read" of read-evaluate-print-loop most definitely
>>>>>> counts as IO :)
>>>>>>
>>>>>>
>>>>> as does the "print"
>>>>>
>>>> It does, but it's not necessary to play.
>>>>
>>>> NW --> empty
>>>>
>>>> Your move.
>>>>
>>>>
>>> How should I enter it? Or know what move you made? Without
>>> inputing somewhere, or reading what you typed and has since
>>> been output to the console.
>>>
>>> If it's not to be done via the repl then the whole thing must
>>> be compiled atomically, with no scope for interaction. Without
>>> interaction, the act of compilation is not playing the game,
>>> it's merely simulating a game that we've already played outside
>>> of the compiler.
>>>
>> 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.
>>
>>
> Returned how? where? to whom?
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.

Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 09:20, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:16, Kevin Wright wrote:
> On 15 February 2011 09:10, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 19:09, Kevin Wright wrote:
>>> On 15 February 2011 09:08, Kevin Wright
>>> <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:
>>>
>>>>
>>>>
>>>> On 15 February 2011 09:05, Tony Morris
>>>> <tonymorris [at] gmail [dot] com> wrote:
>>>>
>>>>>
>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>
>>>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>>>> On 15 February 2011 08:54, Tony Morris
>>>>>> <tonymorris [at] gmail [dot] com> wrote:
>>>>>>
>>>>>>>
>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>
>>>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper Nordenberg
>>>>>>>> <megagurka [at] yahoo [dot] com> wrote:
>>>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>>>
>>>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>>>> <megagurka [at] yahoo [dot] com
>>>>>>>>>> <mailto:megagurka [at] yahoo [dot] com>> wrote:
>>>>>>>>>>> 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.
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>
>>>>>>> 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/
>>>>>>>
>>>>>>>
>>>>>> I'd argue that point... Sure you can "simulate" a game
>>>>>> without IO, but "play" it?
>>>>>>
>>>>>>
>>>>>>> let myMove = NW --> empty :type myMove
>>>>> myMove :: Board
>>>>>
>>>>> Your move.
>>>>>
>>>>> - -- Tony Morris http://tmorris.net/
>>>>>
>>>>>
>>>> The "read" of read-evaluate-print-loop most definitely counts
>>>> as IO :)
>>>>
>>>>
>>> as does the "print"
>>>
>> It does, but it's not necessary to play.
>>
>> NW --> empty
>>
>> Your move.
>>
>>
> How should I enter it? Or know what move you made? Without
> inputing somewhere, or reading what you typed and has since been
> output to the console.
>
> If it's not to be done via the repl then the whole thing must be
> compiled atomically, with no scope for interaction. Without
> interaction, the act of compilation is not playing the game, it's
> merely simulating a game that we've already played outside of the
> compiler.
>
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.


Returned how? where? to whom?
Without IO the returned value only exists in isolation, within the compiler.  It's not something that I as a player can use, just something the compiler can use.
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?
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.
Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 09:36, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 19:28, Kevin Wright wrote:
> On 15 February 2011 09:20, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 19:16, Kevin Wright wrote:
>>> On 15 February 2011 09:10, Tony Morris <tonymorris [at] gmail [dot] com>
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 19:09, Kevin Wright wrote:
>>>>> On 15 February 2011 09:08, Kevin Wright
>>>>> <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:
>>>>>
>>>>>>
>>>>>>
>>>>>> On 15 February 2011 09:05, Tony Morris
>>>>>> <tonymorris [at] gmail [dot] com> wrote:
>>>>>>
>>>>>>>
>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>
>>>>>>> On 15/02/11 19:00, Kevin Wright wrote:
>>>>>>>> On 15 February 2011 08:54, Tony Morris
>>>>>>>> <tonymorris [at] gmail [dot] com> wrote:
>>>>>>>>
>>>>>>>>>
>>>>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>>>>
>>>>>>>>> On 15/02/11 10:40, Jim Powers wrote:
>>>>>>>>>> On Mon, Feb 14, 2011 at 7:31 PM, Jesper
>>>>>>>>>> Nordenberg <megagurka [at] yahoo [dot] com> wrote:
>>>>>>>>>>> Jim Powers skrev 2011-02-15 01:15:
>>>>>>>>>>>>
>>>>>>>>>>>> On Feb 14, 2011 6:36 PM, "Jesper Nordenberg"
>>>>>>>>>>>> <megagurka [at] yahoo [dot] com
>>>>>>>>>>>> <mailto:megagurka [at] yahoo [dot] com>> wrote:
>>>>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>> 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/
>>>>>>>>>
>>>>>>>>>
>>>>>>>> I'd argue that point... Sure you can "simulate" a
>>>>>>>> game without IO, but "play" it?
>>>>>>>>
>>>>>>>>
>>>>>>>>> let myMove = NW --> empty :type myMove
>>>>>>> myMove :: Board
>>>>>>>
>>>>>>> Your move.
>>>>>>>
>>>>>>> - -- Tony Morris http://tmorris.net/
>>>>>>>
>>>>>>>
>>>>>> The "read" of read-evaluate-print-loop most definitely
>>>>>> counts as IO :)
>>>>>>
>>>>>>
>>>>> as does the "print"
>>>>>
>>>> It does, but it's not necessary to play.
>>>>
>>>> NW --> empty
>>>>
>>>> Your move.
>>>>
>>>>
>>> How should I enter it? Or know what move you made? Without
>>> inputing somewhere, or reading what you typed and has since
>>> been output to the console.
>>>
>>> If it's not to be done via the repl then the whole thing must
>>> be compiled atomically, with no scope for interaction. Without
>>> interaction, the act of compilation is not playing the game,
>>> it's merely simulating a game that we've already played outside
>>> of the compiler.
>>>
>> 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.
>>
>>
> Returned how? where? to whom?
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.


It's not always 8 possibilities, it's only 8 if I'm playing the second move and you've already played the first.  So how did I know what my 8 possibilities were, which square I couldn't play, if I hadn't already been made aware of the square you played?  I can't move without foreknowledge of the existing moves, and that foreknowledge comes courtesy of some form of IO.
How, pray tell, can I revisit a type unless it is somehow "output" to me? 
>
> 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.


I'd say it was a crucial distinction.  If two people are playing a game then we'd play it, and afterwards would enter those moves as source code for the compiler to encode.  If playing against the computer, there must be some means for the computer to inform me of the moves and for me to respond.
In the first case, entering the source code is not playing, that's already been done.  In the second case I either need IO or a lot of lucky guesses. 
Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

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

Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 09:54, Tony Morris <tonymorris [at] gmail [dot] 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.
Artem Khodyush
Joined: 2011-02-15,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

> Please see the type

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

On Tue, Feb 15, 2011 at 1:54 AM, Tony Morris 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*.
>
> 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-----
>
>

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:02, Kevin Wright wrote:
> On 15 February 2011 09:54, Tony Morris
> 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.
>
Are you suggesting you need IO in order to come to know the type?

If that's the case, we have even bigger problems.

nicolas.oury@gm...
Joined: 2011-02-13,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing
To clarify, if you write in Agda something along those lines:
playable : Board -> Position -> Bool playable = ... // checks that Position is free in board and that the Board is not a finished game.
So : Bool -> TypeSo true = Unit So false = Nothing
// Use Unit and Nothing to respect the name of their Scala equivalent.  // It needs to be a proof-irrelevant non-empty for true and an empty type for false.
move : (b : Board) -> (p : Position) -> {pre : So (playable b p)} -> Boardmove = ....
With this program, whatever you do in the client code, if the program compile, you know that you will always  move to an empty case on a board still in play.
That will, of course, oblige the client to check that property a la:play : (b : Board) -> (p : Position)  -> IO () play b p with (playable b p)...            | true  =  next-turn (move b p {()}) // So (playable b p) == Unit here...            | false = same-turn b "Please play on a free case"
The same thing could be done in Agda, but the So (playable b p) would have to be encoded entirely at the level of type.And the client code would need to have as many branches as possible position.
match (p,b) with {case (Case1, b:EmptyCase1) => b playCase1; // playCase1 is a method of trait EmptyCase1...case (Case9, ....)}
Or I miss something in the way Scala type system work?
Best regads,
Nicolas


  
Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 10:21, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:18, Kevin Wright wrote:
> On 15 February 2011 10:10, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:02, Kevin Wright wrote:
>>> On 15 February 2011 09:54, Tony Morris <tonymorris [at] gmail [dot] 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.
>>>
>> Are you suggesting you need IO in order to come to know the
>> type?
>>
>> If that's the case, we have even bigger problems.
>>
>>
> I'm suggesting that the only possible way I could know what the
> type is, or even that the type exists, is via some sort of input
> through my brain. Sight, sound, braille, direct electrical
> stimulation, whatever!
>
> The only point at which I can truly be said to be "playing" the
> game is when my brain is involved, and my brain requires input and
> output in order to be able to do that. It's perfectly valid for
> that IO to be nothing more than human conversation followed by
> verbatim entry of the game (input) to some compiler. the compiler
> can then internally reconstruct the pre-existing game requiring no
> further IO.
>
> But the crucial, creative, act of "playing" is interactive and, as
> such, requires IO of some form.
>
We seem to have departed from what I meant by IO.


It was more your definition of "playing" that I found troublesome.  A compiler can certainly do *something* with a list of moves that doesn't involve any IO, but I'd never describe that action as actually playing the game.  
Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 10:10, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:02, Kevin Wright wrote:
> On 15 February 2011 09:54, Tony Morris <tonymorris [at] gmail [dot] 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.
>
Are you suggesting you need IO in order to come to know the type?

If that's the case, we have even bigger problems.


I'm suggesting that the only possible way I could know what the type is, or even that the type exists, is via some sort of input through my brain.  Sight, sound, braille, direct electrical stimulation, whatever!
The only point at which I can truly be said to be "playing" the game is when my brain is involved, and my brain requires input and output in order to be able to do that.  It's perfectly valid for that IO to be nothing more than human conversation followed by verbatim entry of the game (input) to some compiler.  the compiler can then internally reconstruct the pre-existing game requiring no further IO.
But the crucial, creative, act of "playing" is interactive and, as such, requires IO of some form.

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:24, Kevin Wright wrote:
> On 15 February 2011 10:21, Tony Morris
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:18, Kevin Wright wrote:
>>> On 15 February 2011 10:10, Tony Morris
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 20:02, Kevin Wright wrote:
>>>>> On 15 February 2011 09:54, Tony Morris
>>>>> 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.
>>>>>
>>>> Are you suggesting you need IO in order to come to know the
>>>> type?
>>>>
>>>> If that's the case, we have even bigger problems.
>>>>
>>>>
>>> I'm suggesting that the only possible way I could know what
>>> the type is, or even that the type exists, is via some sort of
>>> input through my brain. Sight, sound, braille, direct
>>> electrical stimulation, whatever!
>>>
>>> The only point at which I can truly be said to be "playing"
>>> the game is when my brain is involved, and my brain requires
>>> input and output in order to be able to do that. It's perfectly
>>> valid for that IO to be nothing more than human conversation
>>> followed by verbatim entry of the game (input) to some
>>> compiler. the compiler can then internally reconstruct the
>>> pre-existing game requiring no further IO.
>>>
>>> But the crucial, creative, act of "playing" is interactive and,
>>> as such, requires IO of some form.
>>>
>> We seem to have departed from what I meant by IO.
>>
>>
> It was more your definition of "playing" that I found troublesome.
> A compiler can certainly do *something* with a list of moves that
> doesn't involve any IO, but I'd never describe that action as
> actually playing the game.
>
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 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:18, Kevin Wright wrote:
> On 15 February 2011 10:10, Tony Morris
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:02, Kevin Wright wrote:
>>> On 15 February 2011 09:54, Tony Morris
>>> 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.
>>>
>> Are you suggesting you need IO in order to come to know the
>> type?
>>
>> If that's the case, we have even bigger problems.
>>
>>
> I'm suggesting that the only possible way I could know what the
> type is, or even that the type exists, is via some sort of input
> through my brain. Sight, sound, braille, direct electrical
> stimulation, whatever!
>
> The only point at which I can truly be said to be "playing" the
> game is when my brain is involved, and my brain requires input and
> output in order to be able to do that. It's perfectly valid for
> that IO to be nothing more than human conversation followed by
> verbatim entry of the game (input) to some compiler. the compiler
> can then internally reconstruct the pre-existing game requiring no
> further IO.
>
> But the crucial, creative, act of "playing" is interactive and, as
> such, requires IO of some form.
>
We seem to have departed from what I meant by IO.

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:33, Kevin Wright wrote:
> On 15 February 2011 10:26, Tony Morris
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:24, Kevin Wright wrote:
>>> On 15 February 2011 10:21, Tony Morris
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 20:18, Kevin Wright wrote:
>>>>> On 15 February 2011 10:10, Tony Morris
>>>>> wrote:
>>>>>
>>>>>>
>>>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>>>
>>>>>> On 15/02/11 20:02, Kevin Wright wrote:
>>>>>>> On 15 February 2011 09:54, Tony Morris
>>>>>>> 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.
>>>>>>>
>>>>>> Are you suggesting you need IO in order to come to know
>>>>>> the type?
>>>>>>
>>>>>> If that's the case, we have even bigger problems.
>>>>>>
>>>>>>
>>>>> I'm suggesting that the only possible way I could know
>>>>> what the type is, or even that the type exists, is via some
>>>>> sort of input through my brain. Sight, sound, braille,
>>>>> direct electrical stimulation, whatever!
>>>>>
>>>>> The only point at which I can truly be said to be
>>>>> "playing" the game is when my brain is involved, and my
>>>>> brain requires input and output in order to be able to do
>>>>> that. It's perfectly valid for that IO to be nothing more
>>>>> than human conversation followed by verbatim entry of the
>>>>> game (input) to some compiler. the compiler can then
>>>>> internally reconstruct the pre-existing game requiring no
>>>>> further IO.
>>>>>
>>>>> But the crucial, creative, act of "playing" is interactive
>>>>> and, as such, requires IO of some form.
>>>>>
>>>> We seem to have departed from what I meant by IO.
>>>>
>>>>
>>> It was more your definition of "playing" that I found
>>> troublesome. A compiler can certainly do *something* with a
>>> list of moves that doesn't involve any IO, but I'd never
>>> describe that action as actually playing the game.
>>>
>> We certainly can play a game without IO. You just refused to make
>> your move :)
>>
>>
> Don't be silly, we're using email... that's most definitely IO :)
>
>
>
>> 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.
>
>
> I think the point I was getting at is that in order to do something
> with a computer that *I* would categorize as playing, then it would
> necessarily involve something that *you* would categorize as IO.
> The essence of games is that they are interactive, outside of a
> REPL that's not something you can capture in a type system - which
> typically enshrines the opposite goal, to permanently fix
> invariants outside of any temporal concerns.
>
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 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:44, Steven Obua wrote:
> It seems to me that one of the serious drawbacks of static typing
> has manifested itself: much ado about nothing ;-)
>
> 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
I am high on painkillers at the moment. I shall assume this was a
joke. I hope this is OK with you.

Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing


On 15 February 2011 10:26, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:24, Kevin Wright wrote:
> On 15 February 2011 10:21, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:18, Kevin Wright wrote:
>>> On 15 February 2011 10:10, Tony Morris <tonymorris [at] gmail [dot] com>
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 20:02, Kevin Wright wrote:
>>>>> On 15 February 2011 09:54, Tony Morris
>>>>> <tonymorris [at] gmail [dot] 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.
>>>>>
>>>> Are you suggesting you need IO in order to come to know the
>>>> type?
>>>>
>>>> If that's the case, we have even bigger problems.
>>>>
>>>>
>>> I'm suggesting that the only possible way I could know what
>>> the type is, or even that the type exists, is via some sort of
>>> input through my brain. Sight, sound, braille, direct
>>> electrical stimulation, whatever!
>>>
>>> The only point at which I can truly be said to be "playing"
>>> the game is when my brain is involved, and my brain requires
>>> input and output in order to be able to do that. It's perfectly
>>> valid for that IO to be nothing more than human conversation
>>> followed by verbatim entry of the game (input) to some
>>> compiler. the compiler can then internally reconstruct the
>>> pre-existing game requiring no further IO.
>>>
>>> But the crucial, creative, act of "playing" is interactive and,
>>> as such, requires IO of some form.
>>>
>> We seem to have departed from what I meant by IO.
>>
>>
> It was more your definition of "playing" that I found troublesome.
> A compiler can certainly do *something* with a list of moves that
> doesn't involve any IO, but I'd never describe that action as
> actually playing the game.
>
We certainly can play a game without IO. You just refused to make your
move :)


Don't be silly, we're using email... that's most definitely IO :)
 
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.

I think the point I was getting at is that in order to do something with a computer that *I* would categorize as playing, then it would necessarily involve something that *you* would categorize as IO.  The essence of games is that they are interactive, outside of a REPL that's not something you can capture in a type system - which typically enshrines the opposite goal, to permanently fix invariants outside of any temporal concerns.
phlegmaticprogrammer
Joined: 2010-07-23,
User offline. Last seen 2 years 15 weeks ago.
Re: Re: Benefits of static typing

It seems to me that one of the serious drawbacks of static typing has manifested itself: much ado about nothing ;-)

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

Johannes Rudolph 2
Joined: 2010-02-12,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

On Tue, Feb 15, 2011 at 11:44 AM, Steven Obua
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.

Jim Powers
Joined: 2011-01-24,
User offline. Last seen 36 weeks 2 days ago.
Re: Re: Benefits of static typing

On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
wrote:
> On Tue, Feb 15, 2011 at 11:44 AM, Steven Obua
> 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.

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.

Razvan Cojocaru 3
Joined: 2010-07-28,
User offline. Last seen 42 years 45 weeks ago.
RE: Re: Benefits of static typing

This is proof that email is not type-safe, statically or otherwise :)

-----Original Message-----
From: scala-debate [at] googlegroups [dot] com [mailto:scala-debate [at] googlegroups [dot] com] On Behalf Of Johannes Rudolph
Sent: February-15-11 6:02 AM
To: Steven Obua
Cc: tmorris [at] tmorris [dot] net; Kevin Wright; scala-debate [at] googlegroups [dot] com
Subject: Re: [scala-debate] Re: Benefits of static typing

On Tue, Feb 15, 2011 at 11:44 AM, Steven Obua 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

Kevin Wright 2
Joined: 2010-05-30,
User offline. Last seen 26 weeks 4 days ago.
Re: Re: Benefits of static typing

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?

On 15 February 2011 15:42, Jim Powers <jim [at] casapowers [dot] com> wrote:
On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
<johannes [dot] rudolph [at] googlemail [dot] com> wrote:
> On Tue, Feb 15, 2011 at 11:44 AM, Steven Obua
> <steven [dot] obua [at] googlemail [dot] 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.

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



--
Kevin Wright

gtalk / msn : kev [dot] lee [dot] wright [at] gmail [dot] comkev [dot] lee [dot] wright [at] gmail [dot] commail: kevin [dot] wright [at] scalatechnology [dot] com
vibe / skype: kev.lee.wrightquora: http://www.quora.com/Kevin-Wright
twitter: @thecoda

"My point today is that, if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent": the current conventional wisdom is so foolish as to book that count on the wrong side of the ledger" ~ Dijkstra
fanf
Joined: 2009-03-17,
User offline. Last seen 2 years 30 weeks ago.
Re: Re: Benefits of static typing

On 15/02/2011 16:42, Jim Powers wrote:
> On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
[...]
> "Playing" tic-tac-tow through test cases either exactly expresses
> proof by exhaustive search or approximates it.[...] 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.

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,

Derek Williams
Joined: 2009-06-13,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

On Tue, Feb 15, 2011 at 9:16 AM, Kevin Wright wrote:
> 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/

Jim Powers
Joined: 2011-01-24,
User offline. Last seen 36 weeks 2 days ago.
Re: Re: Benefits of static typing

On Tue, Feb 15, 2011 at 11:28 AM, Francois wrote:
> On 15/02/2011 16:42, Jim Powers wrote:
>>
>> On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
>
> [...]
>>
>> "Playing" tic-tac-tow through test cases either exactly expresses
>> proof by exhaustive search or approximates it.[...]   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.
>
> 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).

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.

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 16/02/11 02:39, Jim Powers wrote:
> On Tue, Feb 15, 2011 at 11:28 AM, Francois
> wrote:
>> On 15/02/2011 16:42, Jim Powers wrote:
>>>
>>> On Tue, Feb 15, 2011 at 6:02 AM, Johannes Rudolph
>>
>> [...]
>>>
>>> "Playing" tic-tac-tow through test cases either exactly
>>> expresses proof by exhaustive search or approximates it.[...]
>>> 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.
>>
>> 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).
>
> 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.
>
I honestly didn't expect the fuss or appeals to mysticism.

Nevertheless, I hope the important point was learned.

jibal
Joined: 2010-12-01,
User offline. Last seen 1 year 45 weeks ago.
Re: Re: Benefits of static typing
On Tue, Feb 15, 2011 at 2:33 AM, Kevin Wright <kev [dot] lee [dot] wright [at] gmail [dot] com> wrote:


On 15 February 2011 10:26, Tony Morris <tonymorris [at] gmail [dot] com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 15/02/11 20:24, Kevin Wright wrote:
> On 15 February 2011 10:21, Tony Morris <tonymorris [at] gmail [dot] com>
> wrote:
>
>>
>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>
>> On 15/02/11 20:18, Kevin Wright wrote:
>>> On 15 February 2011 10:10, Tony Morris <tonymorris [at] gmail [dot] com>
>>> wrote:
>>>
>>>>
>>>> -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
>>>>
>>>> On 15/02/11 20:02, Kevin Wright wrote:
>>>>> On 15 February 2011 09:54, Tony Morris
>>>>> <tonymorris [at] gmail [dot] 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.
>>>>>
>>>> Are you suggesting you need IO in order to come to know the
>>>> type?
>>>>
>>>> If that's the case, we have even bigger problems.
>>>>
>>>>
>>> I'm suggesting that the only possible way I could know what
>>> the type is, or even that the type exists, is via some sort of
>>> input through my brain. Sight, sound, braille, direct
>>> electrical stimulation, whatever!
>>>
>>> The only point at which I can truly be said to be "playing"
>>> the game is when my brain is involved, and my brain requires
>>> input and output in order to be able to do that. It's perfectly
>>> valid for that IO to be nothing more than human conversation
>>> followed by verbatim entry of the game (input) to some
>>> compiler. the compiler can then internally reconstruct the
>>> pre-existing game requiring no further IO.
>>>
>>> But the crucial, creative, act of "playing" is interactive and,
>>> as such, requires IO of some form.
>>>
>> We seem to have departed from what I meant by IO.
>>
>>
> It was more your definition of "playing" that I found troublesome.
> A compiler can certainly do *something* with a list of moves that
> doesn't involve any IO, but I'd never describe that action as
> actually playing the game.
>
We certainly can play a game without IO. You just refused to make your
move :)


Don't be silly, we're using email... that's most definitely IO :)
 
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.

I think the point I was getting at is that in order to do something with a computer that *I* would categorize as playing, then it would necessarily involve something that *you* would categorize as IO.  The essence of games is that they are interactive, outside of a REPL that's not something you can capture in a type system - which typically enshrines the opposite goal, to permanently fix invariants outside of any temporal concerns.
 Consider the fact that, in game theory, one deals with *strategies*, rather than individual moves. So, your strategy must include a response to a board that has an X in NW. You play the game by writing a program that accepts that position, or any other possible position, and returns an appropriate response. Designing such programs with the constraint that programs that don't make legal moves don't compile is well within the game theoretical meaning of "play". Playing in such a way is infeasible for complex games, but Tic-Tac-Toe is a simple enough game that you can keep in your head a strategy that will at least draw in every position and win whenever possible, so it should be easy enough to commit it to a program.

-- Jim
Artem Khodyush
Joined: 2011-02-15,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

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?

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

Are there anything else?

Tony Morris 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

On 16/02/11 10:43, Artem Khodyush wrote:
> 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?
Also, how unnecessary IO can destroy this objective and render an API
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-scal...
>
> 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 2
Joined: 2009-03-20,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Benefits of static typing

On 15/02/11 19:36, Tony Morris wrote:
> 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/Da...

I can also send the scaladoc, however, the types do not enforce a lack
of variables, so it's not as obvious.

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland