Commit cf01477f authored by Vladislav Zavialov's avatar Vladislav Zavialov Committed by Marge Bot
Browse files

User's Guide: KnownNat evidence is Natural

This bit of documentation got outdated after commit
1fcede43
parent 761dcb84
......@@ -259,12 +259,12 @@ Note [KnownNat & KnownSymbol and EvLit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A part of the type-level literals implementation are the classes
"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
defining singleton values. Here is the key stuff from GHC.TypeLits
defining singleton values. Here is the key stuff from GHC.TypeNats
class KnownNat (n :: Nat) where
natSing :: SNat n
newtype SNat (n :: Nat) = SNat Integer
newtype SNat (n :: Nat) = SNat Natural
Conceptually, this class has infinitely many instances:
......@@ -291,10 +291,10 @@ Also note that `natSing` and `SNat` are never actually exposed from the
library---they are just an implementation detail. Instead, users see
a more convenient function, defined in terms of `natSing`:
natVal :: KnownNat n => proxy n -> Integer
natVal :: KnownNat n => proxy n -> Natural
The reason we don't use this directly in the class is that it is simpler
and more efficient to pass around an integer rather than an entire function,
and more efficient to pass around a Natural rather than an entire function,
especially when the `KnowNat` evidence is packaged up in an existential.
The story for kind `Symbol` is analogous:
......
......@@ -10,10 +10,10 @@ Numeric literals are of kind ``Nat``, while string literals are of kind
extension.
The kinds of the literals and all other low-level operations for this
feature are defined in module ``GHC.TypeLits``. Note that the module
defines some type-level operators that clash with their value-level
counterparts (e.g. ``(+)``). Import and export declarations referring to
these operators require an explicit namespace annotation (see
feature are defined in modules ``GHC.TypeLits`` and ``GHC.TypeNats``.
Note that these modules define some type-level operators that clash with their
value-level counterparts (e.g. ``(+)``). Import and export declarations
referring to these operators require an explicit namespace annotation (see
:ref:`explicit-namespaces`).
Here is an example of using type-level numeric literals to provide a
......@@ -59,7 +59,8 @@ a type-level literal. This is done with the functions ``natVal`` and
These functions are overloaded because they need to return a different
result, depending on the type at which they are instantiated. ::
natVal :: KnownNat n => proxy n -> Integer
natVal :: KnownNat n => proxy n -> Natural -- from GHC.TypeNats
natVal :: KnownNat n => proxy n -> Integer -- from GHC.TypeLits
-- instance KnownNat 0
-- instance KnownNat 1
......@@ -79,7 +80,9 @@ will be unknown at compile-time, so it is hidden in an existential type.
The conversion may be performed using ``someNatVal`` for integers and
``someSymbolVal`` for strings: ::
someNatVal :: Integer -> Maybe SomeNat
someNatVal :: Natural -> Maybe SomeNat -- from GHC.TypeNats
someNatVal :: Integer -> Maybe SomeNat -- from GHC.TypeLits
SomeNat :: KnownNat n => Proxy n -> SomeNat
The operations on strings are similar.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment