diff options
| author | HaskellMouse <rinat.stryungis@serokell.io> | 2020-06-19 21:51:59 +0300 |
|---|---|---|
| committer | HaskellMouse <rinat.stryungis@serokell.io> | 2020-10-13 13:05:49 +0300 |
| commit | 8f4f5794eb3504bf2ca093dc5895742395fdbde9 (patch) | |
| tree | 827d862d79d1ff20f4206e225aecb2ca7c1e882a /docs | |
| parent | 0a5f29185921cf2af908988ab3608602bcb40290 (diff) | |
| download | haskell-8f4f5794eb3504bf2ca093dc5895742395fdbde9.tar.gz | |
Unification of Nat and Naturals
This commit removes the separate kind 'Nat' and enables promotion
of type 'Natural' for using as type literal.
It partially solves #10776
Now the following code will be successfully typechecked:
data C = MkC Natural
type CC = MkC 1
Before this change we had to create the separate type for promotion
data C = MkC Natural
data CP = MkCP Nat
type CC = MkCP 1
But CP is uninhabited in terms.
For backward compatibility type synonym `Nat` has been made:
type Nat = Natural
The user's documentation and tests have been updated.
The haddock submodule also have been updated.
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/9.2.1-notes.rst | 16 | ||||
| -rw-r--r-- | docs/users_guide/exts/type_literals.rst | 10 |
2 files changed, 24 insertions, 2 deletions
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst index f8e9853e8f..673fc9f169 100644 --- a/docs/users_guide/9.2.1-notes.rst +++ b/docs/users_guide/9.2.1-notes.rst @@ -28,8 +28,24 @@ Compiler since the argument was already forced in the first equation. For more details see :ghc-flag:`-Wredundant-bang-patterns`. +- Type checker plugins which work with the natural numbers now + should use ``naturalTy`` kind instead of ``typeNatKind``, which has been removed. + ``ghc-prim`` library ~~~~~~~~~~~~~~~~~~~~ - ``Void#`` is now a type synonym for the unboxed tuple ``(# #)``. Code using ``Void#`` now has to enable :extension:`UnboxedTuples`. + +``base`` library +~~~~~~~~~~~~~~~~ + +- It's possible now to promote the ``Natural`` type: :: + + data Coordinate = Mk2D Natural Natural + type MyCoordinate = Mk2D 1 10 + + The separate kind ``Nat`` is removed and now it is just a type synonym for + ``Natural``. As a consequence, one must enable ``TypeSynonymInstances`` + in order to define instances for ``Nat``. + diff --git a/docs/users_guide/exts/type_literals.rst b/docs/users_guide/exts/type_literals.rst index cbf4d89023..202577668d 100644 --- a/docs/users_guide/exts/type_literals.rst +++ b/docs/users_guide/exts/type_literals.rst @@ -5,7 +5,7 @@ Type-Level Literals GHC supports numeric and string literals at the type level, giving convenient access to a large number of predefined type-level constants. -Numeric literals are of kind ``Nat``, while string literals are of kind +Numeric literals are of kind ``Natural``, while string literals are of kind ``Symbol``. This feature is enabled by the :extension:`DataKinds` language extension. @@ -23,11 +23,17 @@ safe interface to a low-level function: :: import Data.Word import Foreign - newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a) + newtype ArrPtr (n :: Natural) a = ArrPtr (Ptr a) clearPage :: ArrPtr 4096 Word8 -> IO () clearPage (ArrPtr p) = ... +Also type-level naturals could be promoted from the ``Natural`` data type +using `DataKinds`, for example: :: + + data Point = MkPoint Natural Natural + type MyCoordinates = MkPoint 95 101 + Here is an example of using type-level string literals to simulate simple record operations: :: |