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

Copyright(C) 2016, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellTrustworthy
LanguageHaskell2010
Extensions
  • UndecidableInstances
  • MonoLocalBinds
  • TemplateHaskell
  • TemplateHaskellQuotes
  • ScopedTypeVariables
  • AllowAmbiguousTypes
  • TypeFamilies
  • TypeInType
  • PolyKinds
  • DataKinds
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll
  • TypeApplications

GHC.TypeLits.KnownNat

Contents

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 Data.Singletons.TH    (genDefunSymbols)
import GHC.TypeLits.KnownNat

$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol

instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where
  type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0
  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

Singleton natural number

newtype SNatKn n Source #

Singleton natural number (represented by an integer)

Constructors

SNatKn Integer 

Constraint-level arithmetic classes

class KnownNat2 f a b 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

Minimal complete definition

natSing2

Associated Types

type KnownNatF2 f :: Nat ~> (Nat ~> Nat) Source #

Methods

natSing2 :: SNatKn ((KnownNatF2 f @@ a) @@ b) Source #

Instances

(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.*" a b Source #

KnownNat2 instance for GHC.TypeLits' *

Associated Types

type KnownNatF2 ("GHC.TypeLits.*" :: Symbol) :: (~>) Nat ((~>) Nat Nat) Source #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.*") a) b) Source #

(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.+" a b Source #

KnownNat2 instance for GHC.TypeLits' +

Associated Types

type KnownNatF2 ("GHC.TypeLits.+" :: Symbol) :: (~>) Nat ((~>) Nat Nat) Source #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.+") a) b) Source #

(KnownNat a, KnownNat b, (<=) b a) => KnownNat2 "GHC.TypeLits.-" a b Source #

KnownNat2 instance for GHC.TypeLits' -

Associated Types

type KnownNatF2 ("GHC.TypeLits.-" :: Symbol) :: (~>) Nat ((~>) Nat Nat) Source #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.-") a) b) Source #

(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.^" a b Source #

KnownNat2 instance for GHC.TypeLits' ^

Associated Types

type KnownNatF2 ("GHC.TypeLits.^" :: Symbol) :: (~>) Nat ((~>) Nat Nat) Source #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.^") a) b) Source #

class KnownNat3 f a b c 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

Minimal complete definition

natSing3

Associated Types

type KnownNatF3 f :: Nat ~> (Nat ~> (Nat ~> Nat)) Source #

Methods

natSing3 :: SNatKn (((KnownNatF3 f @@ a) @@ b) @@ c) Source #

Template Haskell helper

nameToSymbol :: Name -> TypeQ Source #

Convert a TH Name to a type-level Symbol