ghc-typelits-knownnat-0.7.13: Derive KnownNat constraints from other KnownNat constraints

Copyright | (C) 2016 University of Twente 2017-2018 QBayLogic B.V. 2017 Google Inc.
License | BSD2 (see the file LICENSE)
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Extensions

- Cpp
- MonoLocalBinds
- TemplateHaskell
- TemplateHaskellQuotes
- ScopedTypeVariables
- AllowAmbiguousTypes
- TypeFamilies
- GADTs
- GADTSyntax
- PolyKinds
- DataKinds
- TypeSynonymInstances
- FlexibleInstances
- ConstrainedClassMethods
- MultiParamTypeClasses
- MagicHash
- KindSignatures
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll
- TypeApplications

GHC.TypeLits.KnownNat

Contents

- Singleton natural number
- Constraint-level arithmetic classes
- Singleton boolean
- KnownBool
  - Constraint-level boolean functions
- Template Haskell helper

Description

Some "magic" classes and instances to get the GHC.TypeLits.KnownNat.Solver type checker plugin working.

# Usage

Let's say you defined a closed type family `Max`:

    import Data.Type.Bool (If)
    import GHC.TypeLits

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a

if you then want the GHC.TypeLits.KnownNat.Solver to solve `KnownNat` constraints over `Max`, given just `KnownNat` constraints for the arguments of `Max`, then you must define:

    {-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,
                 MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,
                 TypeApplications, TypeFamilies, TypeOperators,
                 UndecidableInstances #-}

    import Data.Proxy            (Proxy (..))
    import GHC.TypeLits.KnownNat

    instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where
      natSing2 = let x = natVal (Proxy a)
                     y = natVal (Proxy b)
                     z = max x y
                 in  SNatKn z
      {-# INLINE natSing2 #-}

# FAQ

#### 1. GHC.TypeLits.KnownNat.Solver does not seem to find the corresponding `KnownNat2` instance for my type-level operation

At the Core-level, GHCs internal mini-Haskell, type families that only have a single equation are treated like type synonyms.

For example, let's say we defined a closed type family `Max`:

    import Data.Type.Bool (If)
    import GHC.TypeLits

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max a b = If (a <=? b) b a

Now, a Haskell-level program might contain a constraint

    KnownNat (Max a b)

, however, at the Core-level, this constraint is expanded to:

    KnownNat (If (a <=? b) b a)

GHC.TypeLits.KnownNat.Solver never sees any reference to the `Max` type family, so it will not look for the corresponding `KnownNat2` instance either. To fix this, ensure that your type-level operations always have at least two equations. For `Max` this means we have to redefine it as:

    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a

Synopsis

- newtype SNatKn (f :: Symbol) = SNatKn Natural
- class KnownNat1 (f :: Symbol) (a :: Nat) where
  - natSing1 :: SNatKn f
- class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where
  - natSing2 :: SNatKn f
- class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where
  - natSing3 :: SNatKn f
- data SBool (b :: Bool) where
  - SFalse :: SBool 'False
  - STrue :: SBool 'True
- boolVal :: forall (b :: Bool) proxy. KnownBool b => proxy b -> Bool
- class KnownBool (b :: Bool) where
  - boolSing :: SBool b
- newtype SBoolKb (f :: Symbol) = SBoolKb Bool
- class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where
  - natBoolSing3 :: SNatKn f
- class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where
  - boolNatSing2 :: SBoolKb f
- nameToSymbol :: Name -> TypeQ

# Singleton natural number

newtype SNatKn (f :: Symbol) Source #

Singleton natural number

Constructors

SNatKn Natural |

# Constraint-level arithmetic classes

class KnownNat1 (f :: Symbol) (a :: Nat) where Source #

Class for arithmetic functions with one argument.

The `Symbol` f must correspond to the fully qualified name of the type-level operation. Use `nameToSymbol` to get the fully qualified TH Name as a `Symbol`

Methods

natSing1 :: SNatKn f Source #

class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where Source #

Class for arithmetic functions with two arguments.

The `Symbol` f must correspond to the fully qualified name of the type-level operation. Use `nameToSymbol` to get the fully qualified TH Name as a `Symbol`

Methods

natSing2 :: SNatKn f Source #

#### Instances

Instances details

(KnownNat a, KnownNat b) => KnownNat2 "GHC.Internal.TypeNats.*" a b Source # | `KnownNat2` instance for GHC.TypeLits' `*`
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.*" Source #
(KnownNat a, KnownNat b) => KnownNat2 "GHC.Internal.TypeNats.+" a b Source # | `KnownNat2` instance for GHC.TypeLits' `+`
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.+" Source #
(KnownNat a, KnownNat b, (b <= a) ~ ()) => KnownNat2 "GHC.Internal.TypeNats.-" a b Source # | `KnownNat2` instance for GHC.TypeLits' `-`
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.-" Source #
(KnownNat x, KnownNat y, (1 <= y) ~ ()) => KnownNat2 "GHC.Internal.TypeNats.Div" x y Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.Div" Source #
(KnownNat x, KnownNat y, (1 <= y) ~ ()) => KnownNat2 "GHC.Internal.TypeNats.Mod" x y Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.Mod" Source #
(KnownNat a, KnownNat b) => KnownNat2 "GHC.Internal.TypeNats.^" a b Source # | `KnownNat2` instance for GHC.TypeLits' `^`
Instance details Defined in GHC.TypeLits.KnownNat Methods natSing2 :: SNatKn "GHC.Internal.TypeNats.^" Source #

class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where Source #

Class for arithmetic functions with three arguments.

The `Symbol` f must correspond to the fully qualified name of the type-level operation. Use `nameToSymbol` to get the fully qualified TH Name as a `Symbol`

Methods

natSing3 :: SNatKn f Source #

# Singleton boolean

data SBool (b :: Bool) where Source #

Singleton version of `Bool`

Constructors

SFalse :: SBool 'False |
STrue :: SBool 'True |

boolVal :: forall (b :: Bool) proxy. KnownBool b => proxy b -> Bool Source #

Get the `Bool` value associated with a type-level `Bool`

Use `boolVal` if you want to perform the standard boolean operations on the reified type-level `Bool`.

Use `boolSing` if you need a context in which the type-checker needs the type-level `Bool` to be either `True` or `False`

    f :: forall proxy b r . KnownBool b => r
    f = case boolSing @b of
      SFalse -> -- context with b ~ False
      STrue  -> -- context with b ~ True

# KnownBool

class KnownBool (b :: Bool) where Source #

Methods

boolSing :: SBool b Source #

#### Instances

Instances details

KnownBool 'False Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods boolSing :: SBool 'False Source #
KnownBool 'True Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods boolSing :: SBool 'True Source #

## Constraint-level boolean functions

newtype SBoolKb (f :: Symbol) Source #

A type "representationally equal" to `SBool`, used for simpler implementation of constraint-level functions that need to create instances of `KnownBool`

Constructors

SBoolKb Bool |

class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where Source #

Class for ternary functions with a Natural result.

The `Symbol` f must correspond to the fully qualified name of the type-level operation. Use `nameToSymbol` to get the fully qualified TH Name as a `Symbol`

Methods

natBoolSing3 :: SNatKn f Source #

#### Instances

Instances details

(KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool "GHC.Internal.Data.Type.Bool.If" a (b :: Nat) (c :: Nat) Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods natBoolSing3 :: SNatKn "GHC.Internal.Data.Type.Bool.If" Source #

class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where Source #

Class for binary functions with a Boolean result.

The `Symbol` f must correspond to the fully qualified name of the type-level operation. Use `nameToSymbol` to get the fully qualified TH Name as a `Symbol`

Methods

boolNatSing2 :: SBoolKb f Source #

#### Instances

Instances details

(KnownNat a, KnownNat b) => KnownBoolNat2 "GHC.Internal.Data.Type.Ord.<=?" (a :: Nat) (b :: Nat) Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods boolNatSing2 :: SBoolKb "GHC.Internal.Data.Type.Ord.<=?" Source #
(KnownNat a, KnownNat b) => KnownBoolNat2 "GHC.Internal.Data.Type.Ord.OrdCond" (a :: Nat) (b :: Nat) Source # |
Instance details Defined in GHC.TypeLits.KnownNat Methods boolNatSing2 :: SBoolKb "GHC.Internal.Data.Type.Ord.OrdCond" Source #

# Template Haskell helper

nameToSymbol :: Name -> TypeQ Source #

Convert a TH `Name` to a type-level `Symbol`