diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2015 Justin Le + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/GHC/TypeLits/List.hs b/src/GHC/TypeLits/List.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/List.hs @@ -0,0 +1,312 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE FlexibleContexts #-} + +-- | +-- Module : GHC.TypeLits.List +-- Description : Typeclasses, singletons, and reifiers for type-level lists +-- of 'Nat's and 'Symbol's. +-- Copyright : (c) Justin Le 2015 +-- License : MIT +-- Maintainer : justin@jle.im +-- Stability : unstable +-- Portability : non-portable +-- +-- +-- Provides the 'KnownNats' and 'KnownSymbols' typeclasses in analogy to +-- 'KnownNat' and 'KnownSymbol' from "GHC.TypeLits". Also provides +-- singleton-esque structures for traversing over type-level lists of +-- 'Nat's and 'Symbol's. Comes with continuation-style reifiers and +-- existential types for dependent typing usage, and as an analogy with +-- 'SomeNat' and 'SomeSymbol'. +-- +-- See typeclass documentations for more information. + +module GHC.TypeLits.List ( + -- * @KnownNats@ + KnownNats(..) + , SomeNats(..) + , NatList(..) + , someNatsVal + , someNatsVal' + , reifyNats + , traverseNatList + , traverseNatList' + , traverseNatList_ + , mapNatList + -- * @KnownSymbols@ + , KnownSymbols(..) + , SomeSymbols(..) + , SymbolList(..) + , someSymbolsVal + , reifySymbols + , traverseSymbolList + , traverseSymbolList' + , traverseSymbolList_ + , mapSymbolList + ) where + +import Data.Proxy +import Data.Reflection +import GHC.TypeLits +import Data.Functor.Identity + +-- | @'KnownNats' ns@ is intended to represent that every 'Nat' in the +-- type-level list 'ns' is itself a 'KnownNat' (meaning, you can use +-- 'natVal' to get its corresponding 'Integer'). +-- +-- In practice, just knowing that every item has a 'KnownNat' instance is +-- not enough; it's nice, but unless you're able to "iterate" over every +-- 'Nat' in the list, it's of limited use. That's why this class also +-- provides a constructor for @'NatList' ns@, so that you can produce +-- a 'NatList' for every @'KnownNat' ns@, which you can iterate over to get +-- @'Proxy' n@s for every 'n' in 'ns' along with the @'KnownNat' n@ +-- instances. +-- +-- It also has an analogy to 'natVal', 'natsVal', which lets you get a list +-- of the represented 'Integer's for, say, @'Proxy' [1,2,3]@. +class KnownNats (ns :: [Nat]) where + natsVal :: p ns -> [Integer] + natsList :: NatList ns + +instance KnownNats '[] where + natsVal _ = [] + natsList = ØNL + +instance (KnownNat n, KnownNats ns) => KnownNats (n ': ns) where + natsVal _ = natVal (Proxy :: Proxy n) : natsVal (Proxy :: Proxy ns) + natsList = Proxy :<# natsList + +-- | Represents unknown type-level lists of type-level natural numbers. +-- It's a 'NatList', but you don't know what the list contains at +-- compile-time. +data SomeNats :: * where + SomeNats :: KnownNats ns => NatList ns -> SomeNats + +-- | Singleton-esque type for "traversing" over type-level lists of 'Nat's. +-- Essentially contains a (value-level) list of @'Proxy' n@s, but each 'n' +-- has a 'KnownNat' instance for you to use. At runtime (after type +-- erasure), is more or less equivalent to a @['Integer']@. +-- +-- Typically generated using 'natsList'. +data NatList :: [Nat] -> * where + ØNL :: NatList '[] + (:<#) :: (KnownNat n, KnownNats ns) => Proxy n -> NatList ns -> NatList (n ': ns) + +infixr 5 :<# +deriving instance Show (NatList ns) + +-- | Utility function for traversing over all of the @'Proxy' n@s in +-- a 'NatList', each with the corresponding 'KnownNat' instance available. +-- Gives the the ability to "change" the represented natural number to +-- a new one, in a 'SomeNat'. +-- +-- Can be considered a form of a @Traversal' 'SomeNat' 'SomeNats'@. +traverseNatList :: forall f ns. Applicative f + => (forall n. KnownNat n => Proxy n -> f SomeNat) + -> NatList ns + -> f SomeNats +traverseNatList f = go + where + go :: forall ms. NatList ms -> f SomeNats + go nl = case nl of + ØNL -> pure $ SomeNats ØNL + p :<# nl' -> merge <$> f p <*> go nl' + merge :: SomeNat -> SomeNats -> SomeNats + merge sn sns = case sn of + SomeNat i -> + case sns of + SomeNats is -> + SomeNats (i :<# is) + +-- | Like 'traverseNatList', but literally actually a +-- @Traversal' 'SomeNat' 'SomeNats'@, so is usable with lens-library +-- machinery. +traverseNatList' :: forall f. Applicative f + => (SomeNat -> f SomeNat) + -> SomeNats + -> f SomeNats +traverseNatList' f ns = + case ns of + SomeNats ns' -> traverseNatList (f . SomeNat) ns' + +-- | Utility function for traversing over all of the @'Proxy' n@s in +-- a 'NatList', each with the corresponding 'KnownNat' instance available. +-- Results are ignored. +traverseNatList_ :: forall f a ns. Applicative f + => (forall n. KnownNat n => Proxy n -> f a) + -> NatList ns + -> f () +traverseNatList_ f = go + where + go :: forall ms. NatList ms -> f () + go nl = case nl of + ØNL -> pure () + p :<# nl' -> f p *> go nl' + +-- | Utility function for \"mapping\" over each of the 'Nat's in the +-- 'NatList'. +mapNatList :: (forall n. KnownNat n => Proxy n -> SomeNat) + -> NatList ns + -> SomeNats +mapNatList f = runIdentity . traverseNatList (Identity . f) + +-- | List equivalent of 'someNatVal'. Convert a list of integers into an +-- unknown type-level list of naturals. Will return 'Nothing' if any of +-- the given 'Integer's is negative. +someNatsVal :: [Integer] -> Maybe SomeNats +someNatsVal [] = Just (SomeNats ØNL) +someNatsVal (n:ns) = do + SomeNat m <- someNatVal n + SomeNats ms <- someNatsVal ns + return $ SomeNats (m :<# ms) + +-- | List equivalent of 'reifyNat'. Given a list of integers, takes +-- a function in an "environment" with a @'NatList' ns@ corresponding to +-- the given list, where every @n@ in @ns@ has a 'KnownNat' instance. +-- +-- Essentially a continuation-style version of 'SomeNats'. +-- +-- For compatability with 'reifyNat', be aware that this also produces +-- @'KnownNat' n@s where @n@ is negative, without complaining. +reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r +reifyNats [] f = f ØNL +reifyNats (n:ns) f = reifyNat n $ \m -> + reifyNats ns $ \ms -> + f (m :<# ms) + +-- | Like 'someNatsVal', but will also go ahead and produce 'KnownNat's +-- whose integer values are negative. It won't ever error on producing +-- them, but extra care must be taken when using the produced 'SomeNat's. +someNatsVal' :: [Integer] -> SomeNats +someNatsVal' ns = reifyNats ns SomeNats + +-- | @'KnownSymbols' ns@ is intended to represent that every 'Symbol' in the +-- type-level list 'ns' is itself a 'KnownSymbol' (meaning, you can use +-- 'symbolVal' to get its corresponding 'String'). +-- +-- You can use 'symbolsVal' to get the corresponding @['String']@ from +-- @'KnownSymbols' ns@. +-- +-- For reasons discussed further in the documentation for 'KnownNats', this +-- also lets you generate a @'SymbolList' ns@, in order to iterate over the +-- type-level list of 'Symbol's and take advantage of their 'KnownSymbol' +-- instances. +class KnownSymbols (ns :: [Symbol]) where + symbolsVal :: p ns -> [String] + symbolsList :: SymbolList ns + +instance KnownSymbols '[] where + symbolsVal _ = [] + symbolsList = ØSL + +instance (KnownSymbol n, KnownSymbols ns) => KnownSymbols (n ': ns) where + symbolsVal _ = symbolVal (Proxy :: Proxy n) : symbolsVal (Proxy :: Proxy ns) + symbolsList = Proxy :<$ symbolsList + +-- | Represents unknown type-level lists of 'Symbol's. It's a 'SymbolList', +-- but you don't know what the list contains at compile-time. +data SomeSymbols :: * where + SomeSymbols :: KnownSymbols ns => SymbolList ns -> SomeSymbols + +-- | Singleton-esque type for "traversing" over type-level lists of +-- 'Symbol's. Essentially contains a (value-level) list of @'Proxy' n@s, +-- but each 'n' has a 'KnownSymbol' instance for you to use. At runtime +-- (after type erasure), is more or less equivalent to a @['String']@. +-- +-- Typically generated using 'symbolsList'. +data SymbolList :: [Symbol] -> * where + ØSL :: SymbolList '[] + (:<$) :: (KnownSymbol n, KnownSymbols ns) => Proxy n -> SymbolList ns -> SymbolList (n ': ns) + +infixr 5 :<$ +deriving instance Show (SymbolList ns) + +-- | Utility function for traversing over all of the @'Proxy' n@s in +-- a 'SymbolList', each with the corresponding 'KnownSymbol' instance +-- available. Gives the the ability to "change" the represented natural +-- number to a new one, in a 'SomeSymbol'. +-- +-- Can be considered a form of a @Traversal' 'SomeSymbol' 'SomeSymbols'@. +traverseSymbolList :: forall f ns. Applicative f + => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol) + -> SymbolList ns + -> f SomeSymbols +traverseSymbolList f = go + where + go :: forall ms. SymbolList ms -> f SomeSymbols + go nl = case nl of + ØSL -> pure $ SomeSymbols ØSL + p :<$ nl' -> merge <$> f p <*> go nl' + merge :: SomeSymbol -> SomeSymbols -> SomeSymbols + merge s sl = case s of + SomeSymbol ps -> + case sl of + SomeSymbols sl' -> + SomeSymbols (ps :<$ sl') + +-- | Like 'traverseSymbolList', but literally actually a +-- @Traversal' 'SomeSymbol' 'SomeSymbols'@, so is usable with lens-library +-- machinery. +traverseSymbolList' :: forall f. Applicative f + => (SomeSymbol -> f SomeSymbol) + -> SomeSymbols + -> f SomeSymbols +traverseSymbolList' f ns = + case ns of + SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns' + +-- | Utility function for traversing over all of the @'Proxy' n@s in +-- a 'SymbolList', each with the corresponding 'KnownSymbol' instance +-- available. Results are ignored. +traverseSymbolList_ :: forall f ns. Applicative f + => (forall n a. KnownSymbol n => Proxy n -> f a) + -> SymbolList ns + -> f () +traverseSymbolList_ f = go + where + go :: forall ms. SymbolList ms -> f () + go nl = case nl of + ØSL -> pure () + p :<$ nl' -> f p *> go nl' + +-- | Utility function for \"mapping\" over each of the 'Symbol's in the +-- 'SymbolList'. +mapSymbolList :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol) + -> SymbolList ns + -> SomeSymbols +mapSymbolList f = runIdentity . traverseSymbolList (Identity . f) + +-- | List equivalent of 'someNatVal'. Convert a list of integers into an +-- unknown type-level list of naturals. Will return 'Nothing' if any of +-- the given 'Integer's is negative. +someSymbolsVal :: [String] -> SomeSymbols +someSymbolsVal [] = SomeSymbols ØSL +someSymbolsVal (n:ns) = + case someSymbolVal n of + SomeSymbol m -> + case someSymbolsVal ns of + SomeSymbols ms -> + SomeSymbols (m :<$ ms) + +-- | List equivalent of 'reifyNat'. Given a list of integers, takes +-- a function in an "environment" with a @'NatList' ns@ corresponding to +-- the given list, where every @n@ in @ns@ has a 'KnownNat' instance. +-- +-- Essentially a continuation-style version of 'SomeSymbols'. +reifySymbols :: [String] + -> (forall ns. KnownSymbols ns => SymbolList ns -> r) + -> r +reifySymbols [] f = f ØSL +reifySymbols (n:ns) f = reifySymbol n $ \m -> + reifySymbols ns $ \ms -> + f (m :<$ ms) diff --git a/src/GHC/TypeLits/Witnesses.hs b/src/GHC/TypeLits/Witnesses.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Witnesses.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PolyKinds #-} + +-- | +-- Module : GHC.TypeLits.Witnesses +-- Description : Instance witnesses for various arithmetic operations on +-- GHC TypeLits. +-- Copyright : (c) Justin Le 2015 +-- License : MIT +-- Maintainer : justin@jle.im +-- Stability : unstable +-- Portability : non-portable +-- +-- +-- This module provides witnesses for instances that result from the +-- various arithmetic operations on GHC TypeLits 'Nat' types. In general, +-- if you have @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@; and if +-- you have @'KnownNat' m@, as well, GHC can't infer @'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 of +-- 'Dict' -> '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. + + +module GHC.TypeLits.Witnesses ( + -- * High level wrapper + withNatOp + -- * Direct witnesses + , natDict + , dictNatVal + -- * Witness generators + , (%+) + , (%-) + , (%*) + , (%^) + -- * Entailments + , entailAdd + , entailSub + , entailMul + , entailExp + ) where + +import Data.Constraint +import GHC.TypeLits +import Data.Proxy +import Data.Reflection +import Unsafe.Coerce + +-- | Create a 'Dict' witness for @'KnownNat' n@. +natDict :: KnownNat n => Proxy n -> Dict (KnownNat n) +natDict _ = Dict + +-- | Get the 'Integer' from the 'KnownNat' instance witnessed by the +-- 'Dict'. +dictNatVal :: forall n. Dict (KnownNat n) -> Integer +dictNatVal Dict = natVal (Proxy :: Proxy n) + +infixl 6 %+ +infixl 6 %- +infixl 7 %* +infixr 8 %^ + +-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates +-- a witness for @'KnownNat' (n + m)@. +-- +-- Follows proper association and fixity for usage with other similar +-- operators. +(%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) +Dict %+ Dict = mapDict entailAdd (Dict :: Dict (KnownNat n, KnownNat m)) + +-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates +-- a witness for @'KnownNat' (n - m)@. +-- +-- Note that this is implemented in a way such that /negative/ 'KnownNat's +-- are produced without any errors. +-- +-- Follows proper association and fixity for usage with other similar +-- operators. +(%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m)) +Dict %- Dict = mapDict entailSub (Dict :: Dict (KnownNat n, KnownNat m)) + +-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates +-- a witness for @'KnownNat' (n * m)@. +-- +-- Follows proper association and fixity for usage with other similar +-- operators. +(%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) +Dict %* Dict = mapDict entailMul (Dict :: Dict (KnownNat n, KnownNat m)) + +-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates +-- a witness for @'KnownNat' (n ^ m)@. +-- +-- Follows proper association and fixity for usage with other similar +-- operators. +(%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m)) +Dict %^ Dict = mapDict entailExp (Dict :: Dict (KnownNat n, KnownNat m)) + +-- | 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 the 'Integer' 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 of +-- 'Dict' -> '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.) +-- +-- +withNatOp :: (KnownNat n, KnownNat m) + => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) + -> Proxy n + -> Proxy m + -> (KnownNat q => r) + -> r +withNatOp op x y r = case natDict x `op` natDict y of + Dict -> r + +-- | An entailment for addition of 'KnownNat' instances. +entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m) +entailAdd = Sub $ + reifyNat (natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy m)) $ \p -> + unsafeCoerce (natDict p) + +-- | An entailment for subtraction of 'KnownNat' instances. +-- +-- Note that this is implemented in a way such that /negative/ 'KnownNat's +-- are produced without any errors. +entailSub :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n - m) +entailSub = Sub $ + reifyNat (natVal (Proxy :: Proxy n) - natVal (Proxy :: Proxy m)) $ \p -> + unsafeCoerce (natDict p) + +-- | An entailment for multiplication of 'KnownNat' instances. +entailMul :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m) +entailMul = Sub $ + reifyNat (natVal (Proxy :: Proxy n) * natVal (Proxy :: Proxy m)) $ \p -> + unsafeCoerce (natDict p) + +-- | An entailment for exponentiation of 'KnownNat' instances. +entailExp :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m) +entailExp = Sub $ + reifyNat (natVal (Proxy :: Proxy n) ^ natVal (Proxy :: Proxy m)) $ \p -> + unsafeCoerce (natDict p) + diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal new file mode 100644 --- /dev/null +++ b/typelits-witnesses.cabal @@ -0,0 +1,46 @@ +name: typelits-witnesses +version: 0.1.0.0 +synopsis: Existential witnesses, singletons, and classes for operations on GHC TypeLits +description: Provides witnesses for 'KnownNat' and 'KnownSymbol' + instances for various operations on GHC TypeLits - in + particular, the arithmetic operations defined in + "GHC.TypeLits", and also for type-level lists of + 'KnownNat' and 'KnownSymbol' instances. + . + This is useful for situations where you have + @'KnownNat' n@, and you want to prove to GHC + @'KnownNat' (n + 3)@, or @'KnownNat' (2*n + 4)@. + . + It's also useful for when you want to work with type + level lists of 'KnownNat' or 'KnownSymbol' instances and + singletons for traversing them, and be able to apply + analogies of 'natVal' and 'symbolVal' to lists with + analogies for 'SomeNat' and 'SomeSymbol'. + . + See README for more information. +homepage: https://github.com/mstksg/typelits-witnesses +license: MIT +license-file: LICENSE +author: Justin Le +maintainer: justin@jle.im +copyright: (c) Justin Le 2015 +category: Data +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +source-repository head + type: git + location: git://github.com/mstksg/typelits-witnesses.git + +library + exposed-modules: GHC.TypeLits.Witnesses + GHC.TypeLits.List + -- other-modules: + -- other-extensions: + build-depends: base >=4.8 && <4.9 + , reflection + , constraints + hs-source-dirs: src + ghc-options: -Wall + default-language: Haskell2010