| Copyright | (C) 2016, University of Twente |
|---|---|
| License | BSD2 (see the file LICENSE) |
| Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
| Extensions |
|
GHC.TypeLits.KnownNat
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
Singleton natural number
Singleton natural number (represented by an 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
Instances
| (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.*" a b Source # |
|
| (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.+" a b Source # |
|
| (KnownNat a, KnownNat b, (<=) b a) => KnownNat2 "GHC.TypeLits.-" a b Source # |
|
| (KnownNat a, KnownNat b) => KnownNat2 "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