-
Notifications
You must be signed in to change notification settings - Fork 74
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Update build history; note spago difference * Add initial explanation for VTAs * Fix monad state instantiation * Fix Effect example * Link to falsify and other prop test links * Link to Free Boolean Cube * fp-ts' migration guide * Add GADT-related link * Fix file name * Update spago/purs to latest
- Loading branch information
1 parent
c140536
commit 749e370
Showing
40 changed files
with
1,098 additions
and
42 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
88 changes: 88 additions & 0 deletions
88
11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/01-Intro.purs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,88 @@ | ||
| module Syntax.Basic.VisibleTypeApplications.Intro where | ||
| {- | ||
| Visible Type Applications is a feature that only works completely | ||
| as of PureScript 0.15.13. While it was supported earlier than that, | ||
| there were a few bugs that hindered its usage. The content in this file | ||
| and those that follow in this folder assume one is using PureScript 0.15.13. | ||
| Sometimes, using polymorphic code can be annoying | ||
| because the compiler cannot infer what type you want to use. -} | ||
|
|
||
| polymorphicCode :: forall pleaseInferThisType. pleaseInferThisType -> Int | ||
| polymorphicCode _someValue = 1 | ||
| {- | ||
| problematicUsage :: Int | ||
| problematicUsage = polymorphicCode [] | ||
| The above code is commented out because it will produce a compiler error. | ||
| The empty array is inferred by the compiler to have the type, | ||
| `forall a. Array a`. Because there are no elements within the | ||
| array, the compiler has no idea what the element type is. So, it infers it | ||
| to the most generic type it can be: `forall a. a`. | ||
| In this situation, we would need to tell the compiler what that type is | ||
| by doing one of two things: | ||
| - indicating what the input type of `polymorphicCode` is | ||
| - indicating what the element type of the empty array is | ||
| There's two ways to tell the compiler what the type should be | ||
| when the compiler cannot figure it out. | ||
| The first way is to add a type annotation (usually after wrapping | ||
| the expression in parenthesis). This is annoying to do because | ||
| of the added parenthesis, two colons, and in some cases the need to | ||
| fully specify all the types of the function or value. -} | ||
|
|
||
| usage_inputType :: Int | ||
| usage_inputType = (polymorphicCode :: Array String -> Int) [] | ||
|
|
||
| usage_elemType :: Int | ||
| usage_elemType = polymorphicCode ([] :: Array String) | ||
| {- | ||
| The second way is using "visible type applications". | ||
| Using `forall someType. someType -> Int` as an example, the | ||
| `forall someType.` part is really a function. We could read the above as | ||
| "Given an argument that is a type (e.g. `String`) rather than a value | ||
| (e.g. "foo"), I will return to you a function that takes a value of that type | ||
| and produce a value of type `Int`." | ||
| "Visible Type Applications" are called thus because these type arguments | ||
| are applied to these kinds of functions, but these applications that were | ||
| previously invisible to the user are now made visible. Put differently, | ||
| the compiler would automatically apply these type arguments but without the | ||
| user's knowledge or input. Now, however, the user can also apply these type arguments. | ||
| Visible Type Applications (or VTAs for short) are opt-in syntax. | ||
| They only work if one writes their `forall` part a specific way | ||
| by adding a `@` character in front of the type variable name | ||
| (e.g. `someType` becomes `@someType`). | ||
| Rewriting `polymorphicCode` to use this opt-in syntax, we get: -} | ||
|
|
||
| polymorphicCode2 :: forall @pleaseInferThisType. pleaseInferThisType -> Int | ||
| polymorphicCode2 _someValue = 1 | ||
|
|
||
| -- And now we can use it by applying the type `String` to that type variable. | ||
| -- We apply the type by putting a `@` character in front of the type name. | ||
| usage2_example :: Int | ||
| usage2_example = polymorphicCode2 @String "bar" | ||
|
|
||
| -- In our original case of using a higher-kinded type (e.g. `Array Int`), | ||
| -- we need to wrap the type in parenthesis. | ||
|
|
||
| usage2_inputType :: Int | ||
| usage2_inputType = polymorphicCode2 @(Array String) [] | ||
|
|
||
| -- Since `[]`'s inferred type is `forall a. Array a` rather than `forall @a. Array a`, | ||
| -- we cannot use VTAs to determine the element type. | ||
| -- This code is commented out because we'll get a compiler error. | ||
| -- usage2_elemType :: Int | ||
| -- usage2_elemType = polymorphicCode2 ([] @String)) | ||
|
|
||
| -- Lastly, if we opt-in to this VTA syntax, we must either use it or not use it doesn't mean we have to use VTAs | ||
| -- to make the function work. The below code is valid | ||
|
|
||
| usage3 :: Int | ||
| usage3 = polymorphicCode2 true |
71 changes: 71 additions & 0 deletions
71
11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/02-Order-Matters.purs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,71 @@ | ||
| module Syntax.Basic.VisibleTypeApplications.OrderMatters where | ||
|
|
||
| -- When we write the following function... | ||
| basicFunction :: Int -> String -> Boolean -> String | ||
| basicFunction _i _s _b = "returned value" | ||
|
|
||
| -- ... we know that the order of the arguments matters. | ||
| -- The below usage is valid | ||
| usage :: String | ||
| usage = basicFunction 1 "foo" false | ||
|
|
||
| -- whereas this one is not because the first argument must be an `Int` | ||
| -- usage2 :: String | ||
| -- usage2 = basicFunction "foo" 1 false | ||
|
|
||
| -- Similarly, because functions are curried, | ||
| -- when we apply just one argument, we get back a function | ||
| -- that takes the remaining arguments | ||
|
|
||
| basicFunction' :: String -> Boolean -> String | ||
| basicFunction' = basicFunction 1 | ||
|
|
||
| -- These same ideas apply to VTAs. Notice below that VTA support is only added | ||
| -- to the second and fourth type variable. | ||
| vtaFunction | ||
| :: forall first @second third @fourth | ||
| . first | ||
| -> second | ||
| -> third | ||
| -> fourth | ||
| -> String | ||
| vtaFunction _first _second _third _fourth = "returned value" | ||
|
|
||
| -- Type-level arguments (e.g. VTAs) are always applied before value-level arguments. | ||
| -- Why? Because those arguments appear earlier in the function. | ||
| -- If we want to use VTAs to specify which types `second` and `fourth` are, | ||
| -- we must apply those type arguments BEFORE applying any value arguments. In other words, | ||
| -- the below code is correct: | ||
|
|
||
| usage3 :: String | ||
| usage3 = vtaFunction @Int @Int "first" 2 "third" 4 | ||
|
|
||
| -- whereas this code would be incorrect: | ||
| -- usage3 :: String | ||
| -- usage3 = vtaFunction "first" @Int 2 "third" @Int 4 | ||
|
|
||
| -- Put differently, we can define a new function by only applying a single type argument. | ||
|
|
||
| vtaFunction' | ||
| :: forall first third fourth | ||
| . first | ||
| -> Int | ||
| -> third | ||
| -> fourth | ||
| -> String | ||
| vtaFunction' = vtaFunction @Int -- force `second` to be `Int` | ||
|
|
||
| -- Or by type-applying multiple arguments | ||
| vtaFunction'' | ||
| :: forall first third | ||
| . first | ||
| -> Int | ||
| -> third | ||
| -> Int | ||
| -> String | ||
| vtaFunction'' = vtaFunction @Int @Int -- force `second` and `fourth` to be `Int` | ||
|
|
||
| -- Note: the astute reader will have noticed that the `@` characters don't appear in | ||
| -- `vtaFunction'` and `vtaFunction''`. Since this is opt-in syntax, one must | ||
| -- opt-in every time a new function is defined, even if that function | ||
| -- is derived from applying one argument to a multi-argument curried function. |
Oops, something went wrong.