[Git][ghc/ghc][wip/known-nat-docs] User's Guide: KnownNat evidence is Natural

[Vladislav Zavialov]

Vladislav Zavialov pushed to branch wip/known-nat-docs at Glasgow Haskell Compiler / GHC


Commits:
f86ccecf by Vladislav Zavialov at 2020-06-14T14:14:49+03:00
User's Guide: KnownNat evidence is Natural

This bit of documentation got outdated after commit
1fcede43d2b30f33b7505e25eb6b1f321be0407f

- - - - -


2 changed files:

- compiler/GHC/Tc/Instance/Class.hs
- docs/users_guide/exts/type_literals.rst


Changes:

=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -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:


=====================================
docs/users_guide/exts/type_literals.rst
=====================================
@@ -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.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f86ccecf5e352fb14375ff012a308b9b77463245

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f86ccecf5e352fb14375ff012a308b9b77463245
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200614/76c13871/attachment-0001.html>