Copyright | (c) Justin Le 2016 |
---|---|
License | MIT |
Maintainer | justin@jle.im |
Stability | unstable |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
This module provides witnesses for instances that result from the
various arithmetic operations on GHC TypeLits Nat
types. In general,
if you have
, GHC can't infer KnownNat
n
; and if
you have KnownNat
(n + 1)
, as well, GHC can't infer KnownNat
m
.KnownNat
(n + m)
This can be extremely annoying when dealing with libraries and
applications where one regularly adds and subtracts type-level nats and
expects KnownNat
instances to follow. For example, vector
concatenation of length-encoded vector types can be:
concat :: (KnownNat
n,KnownNat
m) => Vector n a -> Vector m a -> Vector (n + m) a
But, now n + m
does not have a KnownNat
instance...which makes
operations like this extremely less useful!
At the highest level, this module can be used with withNatOp
:
getDoubled :: forall n.KnownNat
n =>Proxy
n ->Integer
getDoubled p =withNatOp
(%*
) p (Proxy
::Proxy
2) $ natVal (Proxy
::Proxy
(n * 2))
With the final argument of withNatOp
, you can provide a result
computed in an environment where n * 2
is indeed an instance of
KnownNat
.
For more complex usage, you can directly manipulate witnesses and then use them via pattern matching:
let pn =natDict
(Proxy
::Proxy
n) p1 =natDict
(Proxy
::Proxy
1) p2 =natDict
(Proxy
::Proxy
2) in case pn%*
p2%+
p1 ofDict
->natVal
(Proxy
::Proxy
(n * 2 + 1))
In the branch of the case statement, n * 2 + 1
indeed has a KnownNat
instance.
Note that the operators have appropriate fixities to mimic value-level arithmetic operations.
WARNING: %-
and entailSub
are is implemented in a way such
that negative KnownNat
s are produced without any errors. The
production of witnesses and entailments will hold, but be aware that any
functions that rely on KnownNat
instances to be non-negative can
potentially break.
- withNatOp :: (KnownNat n, KnownNat m) => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) -> Proxy n -> Proxy m -> (KnownNat q => r) -> r
- natDict :: KnownNat n => Proxy n -> Dict (KnownNat n)
- dictNatVal :: forall n. Dict (KnownNat n) -> Integer
- (%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m))
- (%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m))
- (%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m))
- (%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m))
- entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
- entailSub :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n - m)
- entailMul :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
- entailExp :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
High level wrapper
withNatOp :: (KnownNat n, KnownNat m) => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) -> Proxy n -> Proxy m -> (KnownNat q => r) -> r Source #
A high-level the interface of this module. Give it one of
the witness-generating operators on KnownNat
s in this module (%+
,
%-
, %*
, or %^
), two Proxy
s containing the KnownNat
s to
be modified, and receive an environment where the result of the
operation (applied to the KnownNat
s) has a KnownNat
instance.
For example, with
withNatOp
(%+
) (Proxy
::Proxy
n) (Proxy
::Proxy
1) r
in r
, n + 1
has a KnownNat
instance:
withNatOp
(%+
) (Proxy
::Proxy
n) (Proxy
::Proxy
1) $natVal
(Proxy
::Proxy
(n + 1)) -- => will return theInteger
correpsonding to n + 1
Normally, if n
is a KnownNat
instance, it is not in general
inferrable that n + 1
also has a KnownNat
instance. This combinator
makes it so.
For multiple operations on values, this can be chained:
withNatOp
(%*
) (Proxy
::Proxy
n) (Proxy
::Proxy
2) $withNatOp
(%+
) (Proxy
::Proxy
(n*2)) (Proxy
::Proxy
1) $natVal
(Proxy
::Proxy
(n * 2 + 1))
But, at this point, it's easier and simpler to just directly use the operators and pattern match:
let pn =natDict
(Proxy
::Proxy
n) p1 =natDict
(Proxy
::Proxy
1) p2 =natDict
(Proxy
::Proxy
2) in case pn%*
p2%+
p1 ofDict
->natVal
(Proxy
::Proxy
(n * 2 + 1))
(Note that associativity and fixity for the witness-generating operators are set to match that of normal addition and multiplication, etc.)
Direct witnesses
Witness generators
(%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) infixl 6 Source #
(%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m)) infixl 6 Source #
(%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) infixl 7 Source #
(%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m)) infixr 8 Source #
Entailments
entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m) Source #
An entailment for addition of KnownNat
instances.