@Ding Well, let’s start with basics then. The stuff you’ve told so far is really interesting. I believe you when you say that it’s difficult to you. Just don’t worry that you would not be smart enough, I think you are. You can see everybody agrees the documentation needs work, and you partially know a lot of this if you’ve learned Elm. If we discuss here about the difficult things, it can be used to improve the documentation and that helps the community to grow.
If we start from the basics, we got type declarations just like in the language you’re coming from. Elm uses a single colon on type declarations. Purescript uses double colon. I think the preferred custom would be use of the single colon because types are important. Though Purescript ended up retrieving this feature from Haskell that uses the single colon differently. Either way it’s ok I guess.
In purescript, you’d be writing:
a :: b
c :: d
Type, b and d in this example, could be thought of as terms that determine how other terms, a and c, should be interpreted.
The game semantic interpretation may be useful here. Types in Purescript can be interpreted as games. Type describes what kind of game you play, and the definition is a strategy that never loses that game.
Now I think this should be checked whether it’s correct. I think that the idea of “not losing” allows you to define strategies that repeat infinitely many times and do everything to stop the game from progressing. The traditional way to explain the interpretation is to say that the definition is a strategy that always wins the game. However it’d be a non-turing-complete language that we’d be describing if you had to always win instead of preventing that you ever lose.
- If we got something like
(Unit), it’s a game where you always win. You don’t need to do anything and you can answer with the (unit). That is, unit is a valid play to Unit, and this may be claimed by writing unit :: Unit.
You can follow this in try.purescript.org, If you like to do that, write in the following to give it a try:
a :: Unit
a = unit
-
If you got (Void), you can’t win. The opponent has (absurd) to defeat you every time. This is useful to know because the sides may switch.
-
forall a. b is a game where the opponent can select the game a and it gets substituted into the game b. You are required to provide a strategy to not lose in any of games that opponent might construct by replacing a with any type.
-
The arrow (a -> b) means for a game where you retrieve a variable to initiate the game (a) with the opponent as many times as you want. You can use those plays to win in the game (b).
In the arrow-game, the opponent must supply a game (a) to obtain a play to the game (b). The game is supplied with the “apply” -syntax. Eg. If the (f)is valid play to (a -> b), and (x) is valid play to (a), then (f x) is valid play to (b).
Examples, here’s the “forall” and arrow together because they appear together a lot. The examples are examples of copycat strategies, you take an opponent’s play, and repeat it against himself:
c :: forall a. a -> a
c x = x
d :: forall a b. a -> b -> a
d x y = x
Also the game where the opponent can’t win may be interesting:
e :: forall a. Void -> a
e x = absurd x
- The record is a game where opponent may challenge you to play multiple games and you have to win them all.
{x :: a, y :: b, z :: c} means you got games a, b and c. The opponent may select the game a with the label .x, and so on.
Below’s an example of a game where opponent is challenged to multiple games with you, here’s also something crucial you already saw earlier. You put the opponent to play against himself and he can’t do anything else but to lose.
h :: forall a b c. {x :: a, y :: b, z :: c} -> b
h record = record.y
Likewise to play such games, you got the record syntax to combine plays:
i :: {x :: Unit, y :: Int}
i = {x: unit, y: 4}
Now, if you understand this, next we can proceed for explanation of the Functor and the fat arrow (=>). We should verify that you understand these things before proceeding there though.
As an exercise, you could try to look at the lines starting with :: and see how far you get. Can you explain what kind of games they represent?
An another exercise, describe an always winning strategy for this game (this means same as giving it a definition that passes a type checker and can be guaranteed to terminate):
s :: forall a b c. (a -> b -> c) -> (a -> b) -> a -> c
Some additional help to building terms in try.purescript.org: If you do this:
s = ?hoo
You get a different error that looks like this:
Hole 'hoo' has the inferred type
(a0 -> b1 -> c2) -> (a0 -> b1) -> a0 -> c2
Now you can start progressing with the solution:
s x = ?hoo
And you again get a different error:
Hole 'hoo' has the inferred type
(a0 -> b1) -> a0 -> c2
in the following context:
x :: a0 -> b1 -> c2
It’s very much like playing some sort of a game.
If you feel something needs further explanation, or it still needs to be simpler, please let me know. I’ll supply with all you need to understand this way to understand Purescript. Also if you feel like it’s a bit silly, well… This is not something I came up with. I learned this and have found this useful, but I may not know how to express how it is useful.
Update: I think it’s about semantics. There is a bunch of PDF slides that say game semantics are a form of denotational semantics. Types have multiple semantics and those can be used to understand what types mean.
Also, how do everybody else think about this? Would this be a good approach to explaining Purescript? I think this is being used to explain formal logic, and I think it does also work here. Or have I mixed it up more?
I’m still confused by many basic syntax. When I see a block of PureScript, the first question come to my mind is: how to distinguish which one is a type, which one is a variable? I don’t know. And it seems that type is using along with variable everywhere, in TypeScript usually I’ll use colon “:” to tell the former is usually a variable and the later is usually a type,
