packages feed

type-level (empty) → 0.1

raw patch · 12 files changed

+1543/−0 lines, 12 filesdep +basedep +ghcdep +template-haskellsetup-changed

Dependencies added: base, ghc, template-haskell

Files

+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and+ SAM Group at the School of Information and Communication  Technology,+ (Royal Institute of Technology, Stockholm, Sweden)+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright+      notice, this list of conditions and the following disclaimer in the+      documentation and/or other materials provided with the distribution.+    * Neither the name of The ForSyDe Team nor the+      names of its contributors may be used to endorse or promote products+      derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS TEAM BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,46 @@+type-level: Type-level programming library++DESCRIPTION+++ This library permits performing computations on the type-level. Type-level + functions are implemented using functional dependencies of multi+ parameter type classes. ++ To date, Booleans and Numerals (Naturals and Positives) are+ supported. With regard to Numerals, there is support for common+ arithmetic operations (addition, substraction, multiplication,+ division, exponientation, logarithm, maximum, comparison, GCD) + over natural numbers (using a decimal representation to make + compile-time errors friendlier).++ Although making use of type-level computations might seem devious and+ obfuscated at first sight, it is indeed useful in practice to implement + lightweight dependent types such us number-parameterized types (e.g. an array + type parameterized by the array's size or a modular group type Zn + parameterized by the modulus).+++DEPENDENCIES+ + type-level depends on GHC (due to the use of Multiparameter Type Classes and + infix type constructors) and Template Haskell++INSTALLATION++to install globally, for the whole system (requires admin permissions):++$ ./Setup.hs configure+$ ./Setup.hs build+$ ./Setup.hs haddock # generate documentation, optional, +                     # requires Haddock > 2.0 due to the use of TH+$ ./Setup.hs install++to install locally and just for your own user:++$ ./Setup.hs configure --prefix=The/selected/local/directory+$ ./Setup.hs build+$ ./Setup.hs haddock  # generate documentation, optional, +                      # requires Haddock > 2.0 due to the use of TH++$ ./Setup.hs install --user
+ Setup.hs view
@@ -0,0 +1,7 @@+#! /usr/bin/env runhaskell+module Main (main) where++import Distribution.Simple++main :: IO ()+main = defaultMain
+ src/Data/TypeLevel.hs view
@@ -0,0 +1,20 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- This module is a wrapper for all the publicly usable types and functions+-- of the type-level library.+-- +-----------------------------------------------------------------------------+module Data.TypeLevel (module Data.TypeLevel.Num, +                       module Data.TypeLevel.Bool) where++import Data.TypeLevel.Num+import Data.TypeLevel.Bool
+ src/Data/TypeLevel/Bool.hs view
@@ -0,0 +1,181 @@+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies,+             Rank2Types, DeriveDataTypeable, FlexibleInstances,+             UndecidableInstances, FlexibleContexts  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Bool+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental (MPTC, non-standarad instances)+-- Portability :  non-portable+--+-- Type-level Booleans.+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Bool (+    -- * Type-level boolean values+    Bool,+    False, false,+    True, true,+    reifyBool,+    -- * Type-level boolean operations+    Not, not,+    And, (&&),+    Or, (||),+    Xor, xor,+    Imp, imp,+    Eq, eq++) where++import Data.Generics (Typeable)+import Prelude hiding (Bool, not, (&&), (||), Eq)+import qualified Prelude as P++------------------------------------+-- Definition of type-level Booleans+------------------------------------++-- | True type-level value+data True deriving Typeable++instance Show True where+ show _ = "True"++-- | True value-level reflecting function+true :: True+true = undefined++-- | False type-level value+data False deriving Typeable++instance Show False where+ show _ = "False"+++-- | False value-level reflecting function+false :: False+false = undefined+++-- | Booleans, internal version+class BoolI b where+ toBool :: b -> P.Bool+++-- To prevent the user from adding new instances to BoolI we do NOT export +-- BoolI itself. Rather, we export the following proxy (Bool). +-- The proxy entails BoolI and so can be used to add BoolI +-- constraints in the signatures. However, all the constraints below+-- are expressed in terms of BoolI rather than the proxy. Thus, even if the +-- user adds new instances to the proxy, it would not matter. +-- Besides, because the following proxy instances are most general,+-- one may not add further instances without the overlapping instances +-- extension.++-- | Type-level Booleans+class BoolI b => Bool b++instance BoolI b => Bool b++instance BoolI True where+ toBool _ = True++instance BoolI False where+ toBool _ = False++-- | Reification function. In CPS style (best possible solution)+reifyBool :: P.Bool -> (forall b . Bool b => b -> r) -> r+reifyBool True  f = f true+reifyBool False f = f false++-------------+-- Operations+-------------++-- | Boolean negation type-level relation. @Not b1 b2@ establishes that+-- @not b1 = b2@+class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1+instance Not False True+instance Not True  False++-- | value-level reflection function for the 'Not' type-level relation+not :: Not b1 b2 => b1 -> b2+not = undefined++-- | 'And' type-level relation. @And b1 b2 b3@ establishes that+--   @b1 && b2 = b3@+class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3+instance And False False False  +instance And False True  False  +instance And True  False False  +instance And True  True  True+++-- | value-level reflection function for the 'And' type-level relation+(&&) :: And b1 b2 b3 => b1 -> b2 -> b3+(&&) = undefined++  +-- | Or type-level relation. @Or b1 b2 b3@ establishes that+--   @b1 || b2 = b3@+class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3+instance Or False False False  +instance Or False True  True  +instance Or True  False True  +instance Or True  True  True+++-- | value-level reflection function for the 'Or' type-level relation+(||) :: Or b1 b2 b3 => b1 -> b2 -> b3+(||) = undefined++-- | Exclusive or type-level relation. @Xor b1 b2 b3@ establishes that+--   @xor b1 b2 = b3@+class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3+instance Xor False False False  +instance Xor False True  True  +instance Xor True  False True  +instance Xor True  True  False++-- | value-level reflection function for the 'Xor' type-level relation+xor :: Xor b1 b2 b3 => b1 -> b2 -> b3+xor = undefined+++-- | Implication type-level relation. @Imp b1 b2 b3@ establishes that+-- @b1 =>b2 = b3@+class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3+instance Imp False False True  +instance Imp False True  True  +instance Imp True  False False  +instance Imp True  True  True+++-- | value-level reflection function for the Imp type-level relation+imp :: Imp b1 b2 b3 => b1 -> b2 -> b3+imp = undefined+++-- Although equality can be defined as the composition of Xor and Not+-- we define it specifically++-- | Boolean equality type-level relation+class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3+instance Eq False False True  +instance Eq False True  False  +instance Eq True  False False  +instance Eq True  True  True+++-- FIXME: eq should be named (==) but it clashes with the (==) defined+--        in Data.TypeLevel.Num . The chosen (and ugly) workaround was +--        to rename it to eq.++-- | value-level reflection function for the 'Eq' type-level relation+eq :: Eq b1 b2 b3 => b1 -> b2 -> b3+eq = undefined+
+ src/Data/TypeLevel/Num.hs view
@@ -0,0 +1,25 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- This module is a wrapper for all the publicly usable numerical types and +-- functions of the type-level library.+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Num + (module Data.TypeLevel.Num.Reps,+  module Data.TypeLevel.Num.Aliases,+  module Data.TypeLevel.Num.Sets,+  module Data.TypeLevel.Num.Ops) where++import Data.TypeLevel.Num.Reps+import Data.TypeLevel.Num.Aliases+import Data.TypeLevel.Num.Sets+import Data.TypeLevel.Num.Ops
+ src/Data/TypeLevel/Num/Aliases.hs view
@@ -0,0 +1,29 @@+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+{-# LANGUAGE TemplateHaskell #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num.Aliases+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (Template Haskell)+--+-- Type synonym aliases of type-level numerals and +-- their value-level reflecting functions. Generated for user convenience.+-- +-- Aliases are generated using binary, octal, decimal and hexadecimal bases.+-- Available aliases cover binaries up to b10000000000, octals up to+-- o10000, decimals up to d5000 and hexadecimals up to h1000 +----------------------------------------------------------------------------+module Data.TypeLevel.Num.Aliases where++import Data.TypeLevel.Num.Reps+import Data.TypeLevel.Num.Aliases.TH (genAliases)+++$(genAliases 1024 4096 5000 4096)++
+ src/Data/TypeLevel/Num/Aliases/TH.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num.Aliases+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (Template Haskell)+--+-- Internal template haskell functions to generate type-level numeral aliases+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Num.Aliases.TH (genAliases, dec2TypeLevel) where++import Language.Haskell.TH++import Data.TypeLevel.Num.Reps++data Base = Bin | Oct | Dec | Hex++base2Int :: Base -> Int+base2Int Bin = 2+base2Int Oct = 8+base2Int Dec = 10+base2Int Hex = 16++-- This module needs to be separated from Data.TypeLevel.Num.Aliases due to+-- a limitation in Template Haskell implementation: +-- "You can only run a function at compile time if it is imported from another +-- module." ++genAliases :: Int -- how many binary aliases +           -> Int -- how many octal aliases+           -> Int -- how many dec aliases+           -> Int -- how many hex aliases+           -> Q [Dec]+genAliases nb no nd nh = genAliases' nb no nd nh (maximum [nb,no,nd,nh])++genAliases' :: Int -- how many binary aliases +            -> Int -- how many octal aliases+            -> Int -- how many dec aliases+            -> Int -- how many hex aliases+            -> Int -- maximum alias+            -> Q [Dec]+-- FIXME: genAliases' is ugly!+genAliases' nb no nd nh curr + | curr < 0 = return []+ | otherwise = +    do rest <- genAliases' nb no nd nh (curr-1)+       -- binaries+       restb <- addAliasBase (curr > nb) ('b' : bStr) ('B' : bStr) rest+       -- octals+       resto <- addAliasBase (curr > no) ('o' : oStr) ('O' : oStr) restb+       -- decimals, we don't aliases of the decimal digits+       -- (they are alredy defined in the representation module)+       restd <- if curr > nd then return resto             +                else do val <- genValAlias ('d' : dStr) decRep+                        typ <- genTypeAlias ('D' : dStr) decRep+                        if (curr < 10) then return $ val : resto+                         else return $ val : typ : resto+       -- hexadicimals+       addAliasBase (curr > no) ('h' : hStr) ('H' : hStr) restd+ + where  -- Add aliases of certain base to the rest of aliases+        addAliasBase cond vStr tStr rest =+          if cond then return rest+          else  do val <- genValAlias vStr decRep+                   typ <- genTypeAlias tStr decRep+                   return $ val : typ : rest++        decRep = dec2TypeLevel curr        ++        bStr = toBase Bin curr+        oStr = toBase Oct curr+        dStr = toBase Dec curr+        hStr = toBase Hex curr++-- | Generate the type-level decimal representation for a value-level +--   natural number. +-- NOTE: This function could be useful by itself avoiding to generate +-- aliases. However, type-splicing is not yet supported by template haskell.+dec2TypeLevel :: Int -> Q Type+dec2TypeLevel n+ | n <  0 = error "natural number expected"+ | n < 10 = let name = case n of+                  0 -> ''D0; 1 -> ''D1; 2 -> ''D2; 3 -> ''D3; 4 -> ''D4+                  5 -> ''D5; 6 -> ''D6; 7 -> ''D7; 8 -> ''D8; 9 -> ''D9+            in conT name          + | otherwise = let (quotient, reminder) = n `quotRem` 10 +                   remType  = dec2TypeLevel reminder+                   quotType = dec2TypeLevel quotient+               in (conT ''(:*)) `appT` quotType `appT` remType+++-- | Generate a decimal type synonym alias+genTypeAlias :: String -> Q Type -> Q Dec+genTypeAlias str t = tySynD name [] t+ where name = mkName $ str++-- | Generate a decimal value-level reflected alias+genValAlias :: String -> Q Type -> Q Dec+genValAlias str t = body+ where name = mkName $ str+       body = valD (varP name) +                   (normalB (sigE [| undefined |] t)) []+++-- | Print an integer in certain base+toBase :: Base  -- base +       -> Int  -- Number to print+       -> String+toBase Dec n = show n+toBase b n+  | n < 0 = '-' : toBase b (- n)+  | n < bi = [int2Char n]+  | otherwise = (toBase b rest) ++ [int2Char currDigit]+   where bi = base2Int b +         (rest, currDigit) = n `quotRem` bi++-- | print the corresponding character of a digit+int2Char ::  Int  -- Number to print+          -> Char+int2Char i + | i' < 10 = toEnum (i'+ 48)+ | otherwise = toEnum (i' + 55)+ where i' = abs i
+ src/Data/TypeLevel/Num/Ops.hs view
@@ -0,0 +1,766 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeOperators,+             FlexibleInstances, FlexibleContexts, UndecidableInstances,+             EmptyDataDecls #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num.Ops+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (MPTC, non-standard instances)+--+-- Type-level numerical operations and its value-level reflection functions.+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Num.Ops + (-- * Successor/Predecessor+  Succ, succ,+  Pred, pred,+  -- * Addition/Subtraction+  Add, (+),+  Sub, (-),+  -- * Multiplication/Division+  Mul, (*),+  Div, div,+  Mod, mod,+  DivMod, divMod,+  IsDivBy, isDivBy,+  -- ** Special efficiency cases+  Mul10, mul10,+  Div10, div10,+  DivMod10, divMod10,+  -- * Exponientiation/Logarithm+  ExpBase, (^),+  LogBase, logBase,+  LogBaseF, logBaseF,+  IsPowOf, isPowOf,+  -- ** Special efficiency cases+  Exp10, exp10,+  Log10, log10,+  -- * Comparison assertions+  -- ** General comparison assertion+  Trich, trich,+  -- *** Type-level values denoting comparison results+  LT, EQ, GT,+  -- ** Abbreviated comparison assertions+  (:==:), (:>:), (:<:), (:>=:), (:<=:),+  (==)  , (>)  , (<)  , (>=)  , (<=), +  -- * Maximum/Minimum+  Max, max,+  Min, min,+  -- * Greatest Common Divisor+  GCD, gcd+ ) where++import Data.TypeLevel.Num.Reps+import Data.TypeLevel.Num.Sets+import Data.TypeLevel.Bool++import Prelude hiding + (succ, pred, (+), (-), (*), div, mod, divMod, (^), logBase,+  (==), (>), (<), (<), (>=), (<=), max, min, gcd, Bool)++-------------------------+-- Successor, Predecessor+-------------------------++-- | Successor type-level relation. @Succ x y@ establishes+--  that @succ x = y@.+class (Nat x, Pos y) => Succ x y | x -> y, y -> x+++instance (Pos y, IsZero y yz, DivMod10 x xi xl, Succ' xi xl yi yl yz,+         DivMod10 y yi yl)+   => Succ x y++class Succ' xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xl+++-- This intends to implement a user reporting operation when+-- trying to calculate the predecesor of 0+-- FIXME: however, the instance rule is never triggered!++class Failure t+-- No instances+data PredecessorOfZeroError t+ +instance Failure (PredecessorOfZeroError x) => Succ' (x,x) (x,x) D0 D0 True+instance Succ' xi D0 xi D1 False+instance Succ' xi D1 xi D2 False+instance Succ' xi D2 xi D3 False+instance Succ' xi D3 xi D4 False+instance Succ' xi D4 xi D5 False+instance Succ' xi D5 xi D6 False+instance Succ' xi D6 xi D7 False+instance Succ' xi D7 xi D8 False+instance Succ' xi D8 xi D9 False+instance Succ xi yi => Succ' xi D9 yi D0 False+++{-++Nicer, but not relational implementation of Succ++class (Nat x, Pos y) => Succ' x y | x -> y++-- by structural induction on the first argument+instance Succ' D0 D1+instance Succ' D1 D2+instance Succ' D2 D3+instance Succ' D3 D4+instance Succ' D4 D5+instance Succ' D5 D6+instance Succ' D6 D7+instance Succ' D7 D8+instance Succ' D8 D9+instance Succ' D9 (D1 :* D0)+instance Pos x => Succ' (x :* D0) (x :* D1)+instance Pos x => Succ' (x :* D1) (x :* D2)+instance Pos x => Succ' (x :* D2) (x :* D3)+instance Pos x => Succ' (x :* D3) (x :* D4)+instance Pos x => Succ' (x :* D4) (x :* D5)+instance Pos x => Succ' (x :* D5) (x :* D6)+instance Pos x => Succ' (x :* D6) (x :* D7)+instance Pos x => Succ' (x :* D7) (x :* D8)+instance Pos x => Succ' (x :* D8) (x :* D9)+instance (Pos x, Succ' x y) => Succ' (x :* D9) (y  :* D0)+++class (Nat x, Pos y) => Succ x y | x -> y, y -> x+instance Succ' x y => Succ x y+-}++-- | value-level reflection function for the 'Succ' type-level relation+succ :: Succ x y => x -> y+succ = undefined++-- Note: maybe redundant +-- | Predecessor type-level relation. @Pred x y@ establishes+--  that @pred x = y@.+class (Pos x, Nat y) => Pred x y | x -> y, y -> x+instance Succ x y => Pred y x++-- | value-level reflection function for the 'Pred' type-level relation+pred :: Pred x y => x -> y+pred = undefined++++--------------------+-- Add and Subtract+--------------------+++class (Nat x, Nat y, Nat z) => Add' x y z | x y -> z, z x -> y++-- by structural induction on the first argument+instance Nat y   => Add' D0 y y+instance Succ y z => Add' D1 y z+instance (Succ z z', Add' D1 y z) => Add' D2 y z'+instance (Succ z z', Add' D2 y z) => Add' D3 y z'+instance (Succ z z', Add' D3 y z) => Add' D4 y z'+instance (Succ z z', Add' D4 y z) => Add' D5 y z'+instance (Succ z z', Add' D5 y z) => Add' D6 y z'+instance (Succ z z', Add' D6 y z) => Add' D7 y z'+instance (Succ z z', Add' D7 y z) => Add' D8 y z'+instance (Succ z z', Add' D8 y z) => Add' D9 y z'+-- multidigit addition+-- TODO: explain+instance (Pos (xi :* xl), Nat z,+          Add' xi yi zi, DivMod10 y yi yl, Add' xl (zi :* yl) z)+    => Add' (xi :* xl) y z++-- | Addition type-level relation.  @Add x y z@ establishes+--  that @x + y = z@.+class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x+instance (Add' x y z, Add' y x z) => Add x y z+++-- | value-level reflection function for the 'Add' type-level relation +(+) :: (Add x y z) => x -> y -> z+(+) = undefined++-- | Subtraction type-level relation. @Sub x y z@ establishes+--  that @x - y = z@ +class Sub x y z | x y -> z, z x -> y, z y -> x+instance Add x y z => Sub z y x++-- | value-level reflection function for the 'Sub' type-level relation +(-) :: (Sub x y z) => x -> y -> z+(-) = undefined++------------------------------+-- Multiplication and Division+------------------------------++-----------------+-- Multiplication+-----------------++-- | Multiplication type-level relation. @Mul x y z@ establishes+--  that @x * y = z@.+--   Note it isn't relational (i.e. its inverse cannot be used for division,+--   however, even if it could, the resulting division would only+--   work for zero-remainder divisions)+class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z++-- By structural induction on the first argument+instance Nat y => Mul D0 y D0+instance Nat y => Mul D1 y y+instance Add y y z => Mul D2 y z+-- IMPORTANT: changing the line above by the commented line below+--            would make multiplication relational. However, that would+--            happen at the cost of performing a division by 2 in every +--            multiplication which doesn't pay off.+--            Besides, the Division algortihm obtained out of the +--            inverse of Mul can only work when the remainder is zero, +--            which isn't really useful.+-- instance (Add y y z, DivMod z D2 y D0) => Mul D2 y z+instance (Add z y z', Mul D2 y z) => Mul D3 y z'+instance (Add z y z', Mul D3 y z) => Mul D4 y z'+instance (Add z y z', Mul D4 y z) => Mul D5 y z'+instance (Add z y z', Mul D5 y z) => Mul D6 y z'+instance (Add z y z', Mul D6 y z) => Mul D7 y z'+instance (Add z y z', Mul D7 y z) => Mul D8 y z'+instance (Add z y z', Mul D8 y z) => Mul D9 y z'+-- TODO explain.+instance (Pos (xi :* xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, +          Add dy z10 z')  => Mul (xi :* xl) y z'+++-- | value-level reflection function for the multiplication type-level relation +(*) :: Mul x y z => x -> y -> z+(*) = undefined+++-----------+-- Division+-----------++-- | Division and Remainder type-level relation. @DivMod x y q r@ establishes+--  that @x/y = q + r/y@+--   Note it is not relational (i.e. its inverse cannot be used +--   for multiplication). +class (Nat x, Pos y) =>  DivMod x y q r | x y -> q r+instance (Pos y, Trich x y cmp, DivMod' x y q r cmp) => DivMod x y q r++class (Nat x, Pos y) => DivMod' x y q r cmp | x y cmp -> q r, +                                              q r cmp y -> x,+                                              q r cmp x -> y +instance (Nat x, Pos y) => DivMod' x y D0 x  LT+instance (Nat x, Pos y) => DivMod' x y D1 D0 EQ+instance (Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) +  => DivMod' x y q r GT++-- | value-level reflection function for the 'DivMod' type-level relation+divMod :: DivMod x y q r => x -> y -> (q,r)+divMod _ _ = (undefined, undefined)++-- | Division type-level relation. Remainder-discarding version of 'DivMod'. +--   Note it is not relational (due to DivMod not being relational)+class Div x y z | x y -> z, x z -> y, y z -> x+instance (DivMod x y q r) => Div x y q++-- | value-level reflection function for the 'Div' type-level relation +div :: Div x y z => x -> y -> z+div = undefined++-- | Remainder of division, type-level relation. @Mod x y r@ establishes that+--   @r@ is the reminder of dividing @x@ by @y@.+class Mod x y r | x y -> r+instance DivMod x y q r => Mod x y r++-- | value-level reflection function for the 'Mod' type-level relation +mod :: Mod x y r => x -> y -> r+mod = undefined+++----------------------------------------+-- Multiplication/Division special cases+----------------------------------------++-- | Multiplication by 10 type-level relation (based on 'DivMod10').+--   @Mul10 x y@ establishes that @10 * x = y@.+class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x+instance DivMod10 x q D0 => Mul10 q x++-- | value-level reflection function for 'Mul10' +mul10 :: Mul10 x q => x -> q+mul10 = undefined++-- | Division by 10 and Remainer type-level relation (similar to 'DivMod'). +--+--   This operation is much faster than DivMod. Furthermore, it is +--   the general, non-structural, constructor/deconstructor since it+--   splits a decimal numeral into its initial digits and last digit.+--   Thus, it allows to inspect the structure of a number and is normally+--   used to create type-level operations.+--+--   Note that contrary to 'DivMod', 'DivMod10' is relational (it can be used to+--   multiply by 10)+class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l+instance DivMod10 D0 D0 D0+instance DivMod10 D1 D0 D1+instance DivMod10 D2 D0 D2+instance DivMod10 D3 D0 D3+instance DivMod10 D4 D0 D4+instance DivMod10 D5 D0 D5+instance DivMod10 D6 D0 D6+instance DivMod10 D7 D0 D7+instance DivMod10 D8 D0 D8+instance DivMod10 D9 D0 D9+instance (Nat (D1 :* l)) => DivMod10 (D1 :* l) D1 l  +instance (Nat (D2 :* l)) => DivMod10 (D2 :* l) D2 l  +instance (Nat (D3 :* l)) => DivMod10 (D3 :* l) D3 l  +instance (Nat (D4 :* l)) => DivMod10 (D4 :* l) D4 l  +instance (Nat (D5 :* l)) => DivMod10 (D5 :* l) D5 l  +instance (Nat (D6 :* l)) => DivMod10 (D6 :* l) D6 l +instance (Nat (D7 :* l)) => DivMod10 (D7 :* l) D7 l  +instance (Nat (D8 :* l)) => DivMod10 (D8 :* l) D8 l  +instance (Nat (D9 :* l)) => DivMod10 (D9 :* l) D9 l  +instance (Nat (x :* l), Nat ((x :* l) :* l')) => +  DivMod10 ((x :* l) :* l') (x :* l) l' ++-- | value-level reflection function for DivMod10 +divMod10 :: DivMod10 x q r => x -> (q,r)+divMod10 _ = (undefined, undefined)+++-- | Division by 10 type-level relation (based on DivMod10)+class (Nat x, Nat q) => Div10 x q | x -> q, q -> x+instance DivMod10 x q r => Div10 x q++-- | value-level reflection function for Mul10 +div10 :: Div10 x q => x -> q+div10 = undefined++----------------------------+-- Is-Divisible-By assertion+----------------------------++-- | Is-divisible-by type-level assertion. e.g @IsDivBy d x@ establishes that+--   @x@ is divisible by @d@.+class (Pos d, Nat x) => IsDivBy d x+instance (DivMod x d q D0) => IsDivBy d x++-- | value-level reflection function for IsDivBy+isDivBy :: IsDivBy d x => d -> x+isDivBy = undefined++---------------------------+-- Exponentiation/Logarithm+---------------------------++-- | Exponentation type-level relation. @ExpBase b e r@ establishes+--  that @b^e = r@+--  Note it is not relational (i.e. it cannot be used to express logarithms)+class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r++-- structural induction over the exponent+instance Nat b => ExpBase b D0 D1+instance Nat b => ExpBase b D1 b+instance (Mul b b r) => ExpBase b D2 r+instance (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'+instance (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'+instance (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'+instance (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'+instance (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'+instance (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'+instance (Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'+instance (Nat b, Pos (ei :* el), Nat r, +          Mul b r r', Pred (ei :* el) e', ExpBase b e' r) +           => ExpBase b (ei :* el) r'+-- | value-level reflection function for the ExpBase type-level relation+(^) :: ExpBase b e r => b -> e -> r+(^) = undefined+++-- Logarithm type-level relation. @LogBase b x e@ establishes that +-- @log_base_b x = e@+--  Note it is not relational (i.e. cannot be used to express exponentiation)+class (Pos b, b :>=: D2, Pos x, Nat e) =>  LogBase b x e  | b x -> e +instance  LogBaseF b x e f => LogBase b x e+++-- | value-level reflection function for LogBase+logBase :: LogBaseF b x e f => b -> x -> e+logBase = undefined +++-- | Version of LogBase which also outputs if the logarithm+-- calculated was exact.+-- f indicates if the resulting logarithm has no fractional part (i.e.+-- tells if the result provided is exact)+class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) +     =>  LogBaseF b x e f | b x -> e f+instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f++class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)+     => LogBaseF' b x e f cmp | b x cmp -> e f +instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT+instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True  EQ+instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, +          Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT++-- | value-level reflection function for LogBaseF+logBaseF :: LogBaseF b x e f => b -> x -> (e,f)+logBaseF _ _ = (undefined, undefined) +++-- We could reuse LogBaseF for IsPowOf but it would be inneficient.+-- LogBaseF continues calculating the logarithm even if after knowing its+-- not exact. Thus, it is desirable to include a custom definition of+-- IsPowOf which can "abort" the calculation forcing the Divisions to be+-- exact+++-- | Assert that a number (@x@) can be expressed as the power of another one+--   (@b@) (i.e. the fractional part of @log_base_b x = 0@, or, +--   in a different way, @exists y . b\^y = x@). +class (Pos b, b :>=: D2, Pos x) =>  IsPowOf b x+instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x++class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp+-- If lower (x < b), then the logarithm is not exact  +-- instance (Pos b, b :>=: D2, Pos x) => IsPowOf' b x LT+instance (Pos b, b :>=: D2) => IsPowOf' b b EQ+instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) +         => IsPowOf' b x  GT+-- | +isPowOf :: IsPowOf b x => b -> x -> ()+isPowOf = undefined++-----------------------------------+-- Base-10 Exponentiation/Logarithm+-----------------------------------++-- | Base-10 Exponentiation type-level relation+class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x+instance Exp10 D0 D1+instance Exp10 D1 (D1 :* D0)+instance Exp10 D2 (D1 :* D0 :* D0)+instance Exp10 D3 (D1 :* D0 :* D0 :* D0)+instance Exp10 D4 (D1 :* D0 :* D0 :* D0 :* D0)+instance Exp10 D5 (D1 :* D0 :* D0 :* D0 :* D0 :* D0)+instance Exp10 D6 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+instance Exp10 D7 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+instance Exp10 D8 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+instance Exp10 D9 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+instance (Pred (xi :* xl) x', +          Exp10 x' (y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0))+      => Exp10 (xi :* xl) +               (y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)++-- | value-level reflection function for Exp10+exp10 :: Exp10 x y => x -> y+exp10 = undefined++-- | Base-10 logarithm type-level relation+--   Note it is not relational (cannot be used to express Exponentation to 10)+--   However, it works with any positive numeral (not just powers of 10)+class (Pos x, Nat y) => Log10 x y | x -> y+instance Log10 D1 D0+instance Log10 D2 D0+instance Log10 D3 D0+instance Log10 D4 D0+instance Log10 D5 D0+instance Log10 D6 D0+instance Log10 D7 D0+instance Log10 D8 D0+instance Log10 D9 D0+instance (Pos (xi :* xl), Pred y y', Log10 xi y') => Log10 (xi :* xl) y++-- | value-level reflection function for 'Log10'+log10 :: Log10 x y => x -> y+log10 = undefined++{- Log10': Alternative implementation of Log10++Relational, but it only works for results of Exp10 (i.e. powers of 10).++class (Pos x, Nat y) => Log10' x y | x -> y, y -> x+instance Exp10 x y => Log10' y x+-}+++-------------+-- Comparison+-------------++-- type-level values denoting comparison results++-- | Lower than +data LT+-- | Equal+data EQ+-- | Greater than+data GT++-- | Trichotomy type-level relation. 'Trich x y r' establishes+--   the relation (@r@) between @x@ and @y@. The obtained relation (@r@)+--   Can be 'LT' (if @x@ is lower than @y@), 'EQ' (if @x@ equals @y@) or+--   'GT' (if @x@ is greater than @y@)+class (Nat x, Nat y) => Trich x y r | x y -> r++-- | value-level reflection function for the comparison type-level assertion +trich :: Trich x y r => z -> x -> r+trich = undefined++-- by structural induction on the first, and then the second argument+-- D0+instance Trich D0 D0 EQ+instance Trich D0 D1 LT+instance Trich D0 D2 LT+instance Trich D0 D3 LT+instance Trich D0 D4 LT+instance Trich D0 D5 LT+instance Trich D0 D6 LT+instance Trich D0 D7 LT+instance Trich D0 D8 LT+instance Trich D0 D9 LT+instance Pos (yi :* yl) => Trich D0 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D0 GT+-- D1+instance Trich D1 D0 GT+instance Trich D1 D1 EQ+instance Trich D1 D2 LT+instance Trich D1 D3 LT +instance Trich D1 D4 LT+instance Trich D1 D5 LT +instance Trich D1 D6 LT+instance Trich D1 D7 LT +instance Trich D1 D8 LT+instance Trich D1 D9 LT+instance Pos (yi :* yl) => Trich D1 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D1 GT+-- D2+instance Trich D2 D0 GT+instance Trich D2 D1 GT+instance Trich D2 D2 EQ+instance Trich D2 D3 LT+instance Trich D2 D4 LT+instance Trich D2 D5 LT+instance Trich D2 D6 LT+instance Trich D2 D7 LT+instance Trich D2 D8 LT+instance Trich D2 D9 LT+instance Pos (yi :* yl) => Trich D2 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D2 GT+-- D3+instance Trich D3 D0 GT+instance Trich D3 D1 GT+instance Trich D3 D2 GT+instance Trich D3 D3 EQ+instance Trich D3 D4 LT+instance Trich D3 D5 LT+instance Trich D3 D6 LT+instance Trich D3 D7 LT+instance Trich D3 D8 LT+instance Trich D3 D9 LT+instance Pos (yi :* yl) => Trich D3 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D3 GT+-- D4+instance Trich D4 D0 GT+instance Trich D4 D1 GT+instance Trich D4 D2 GT+instance Trich D4 D3 GT+instance Trich D4 D4 EQ+instance Trich D4 D5 LT+instance Trich D4 D6 LT+instance Trich D4 D7 LT+instance Trich D4 D8 LT+instance Trich D4 D9 LT+instance Pos (yi :* yl) => Trich D4 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D4 GT+-- D5+instance Trich D5 D0 GT+instance Trich D5 D1 GT+instance Trich D5 D2 GT+instance Trich D5 D3 GT+instance Trich D5 D4 GT+instance Trich D5 D5 EQ+instance Trich D5 D6 LT+instance Trich D5 D7 LT+instance Trich D5 D8 LT+instance Trich D5 D9 LT+instance Pos (yi :* yl) => Trich D5 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D5 GT+-- D6+instance Trich D6 D0 GT+instance Trich D6 D1 GT+instance Trich D6 D2 GT+instance Trich D6 D3 GT+instance Trich D6 D4 GT+instance Trich D6 D5 GT+instance Trich D6 D6 EQ+instance Trich D6 D7 LT+instance Trich D6 D8 LT+instance Trich D6 D9 LT+instance Pos (yi :* yl) => Trich D6 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D6 GT+-- D7+instance Trich D7 D0 GT+instance Trich D7 D1 GT+instance Trich D7 D2 GT+instance Trich D7 D3 GT+instance Trich D7 D4 GT+instance Trich D7 D5 GT+instance Trich D7 D6 GT+instance Trich D7 D7 EQ+instance Trich D7 D8 LT+instance Trich D7 D9 LT+instance Pos (yi :* yl) => Trich D7 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D7 GT+-- D8+instance Trich D8 D0 GT+instance Trich D8 D1 GT+instance Trich D8 D2 GT+instance Trich D8 D3 GT+instance Trich D8 D4 GT+instance Trich D8 D5 GT+instance Trich D8 D6 GT+instance Trich D8 D7 GT+instance Trich D8 D8 EQ+instance Trich D8 D9 LT+instance Pos (yi :* yl) => Trich D8 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D8 GT+-- D9+instance Trich D9 D0 GT+instance Trich D9 D1 GT+instance Trich D9 D2 GT+instance Trich D9 D3 GT+instance Trich D9 D4 GT+instance Trich D9 D5 GT+instance Trich D9 D6 GT+instance Trich D9 D7 GT+instance Trich D9 D8 GT+instance Trich D9 D9 EQ+instance Pos (yi :* yl) => Trich D9 (yi :* yl) LT+instance Pos (yi :* yl) => Trich (yi :* yl) D9 GT+++-- multidigit comparison+instance (Pos (xi :* xl), Pos (yi :* yl), Trich xl yl rl, Trich xi yi ri,+	  CS ri rl r) => Trich (xi :* xl) (yi :* yl) r++-- strengthen the comparison relation+class CS r1 r2 r3 | r1 r2 -> r3+instance CS EQ r r+instance CS GT r GT+instance CS LT r LT++-- Abbreviated comparison assertions++-- | Equality abbreviated type-level assertion+class x :==: y+instance (Trich x y EQ) => (:==:) x y -- ??? x :==: y fires an error +                                         -- with ghc 6.8.2 ++-- | value-level reflection function for the equality abbreviated +--   type-level assertion +(==) :: (x :==: y) => x -> y -> ()+(==) = undefined++-- | Greater-than abbreviated type-level assertion+class x :>: y+instance (Trich x y GT) => (:>:) x y ++-- | value-level reflection function for the equality abbreviated +--   type-level assertion +(>) :: (x :>: y) => x -> y -> ()+(>) = undefined++-- | Lower-than abbreviated type-level assertion+class x :<: y+instance (Trich x y LT) => (:<:) x y ++-- | value-level reflection function for the lower-than abbreviated +--   type-level assertion +(<) :: (x :<: y) => x -> y -> ()+(<) = undefined++-- | Greater-than or equal abbreviated type-level assertion+class x :>=: y+instance (Succ x x', Trich x' y GT) => (:>=:) x y ++-- | value-level reflection function for the greater-than or equal abbreviated +--   type-level assertion +(>=) :: (x :>=: y) => x -> y -> ()+(>=) = undefined++-- | Lower-than or equal abbreviated type-level assertion+class x :<=: y+instance (Succ x' x, Trich x' y LT) => (:<=:) x y++-- | value-level reflection function for the lower-than or equal abbreviated +--   type-level assertion +(<=) :: (x :<=: y) => x -> y -> ()+(<=) = undefined++------------------+-- Maximum/Minimum+------------------++-- Choose the largest of x and y in the order b+class Max' x y b r | x y b -> r+instance Max' x y LT y+instance Max' x y EQ y+instance Max' x y GT x++-- | Maximum type-level relation+class Max x y z | x y -> z+instance (Max' x y b z, Trich x y b) => Max x y z++-- | value-level reflection function for the maximum type-level relation+max :: Max x y z => x -> y -> z+max = undefined++-- | Minimum type-level relation+class Min x y z | x y -> z+instance (Max' y x b z, Trich x y b) => Min x y z+++-- | value-level reflection function for the minimum type-level relation+min :: Min x y z => x -> y -> z+min = undefined++-------+-- GCD+-------++-- | Greatest Common Divisor type-level relation+class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd+instance (Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd)+   => GCD x y gcd++-- Euclidean algorithm +class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd+instance Nat x => GCD' x D0 True cmp D0+instance (Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd+instance Nat x => GCD' x x  False EQ x+instance (Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd++-- | value-level reflection function for the GCD type-level relation+gcd :: GCD x y z => x -> y -> z+gcd = undefined++---------------------+-- Internal functions+---------------------++-- classify a natural as positive or zero+class IsZero x r | x -> r+instance IsZero D0 True+instance IsZero D1 False+instance IsZero D2 False+instance IsZero D3 False+instance IsZero D4 False+instance IsZero D5 False+instance IsZero D6 False+instance IsZero D7 False+instance IsZero D8 False+instance IsZero D9 False+instance Pos x => IsZero (x :* d) False
+ src/Data/TypeLevel/Num/Reps.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE EmptyDataDecls, TypeOperators, DeriveDataTypeable,+             ScopedTypeVariables, TemplateHaskell #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num.Reps+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (TypeOperators)+--+-- Type-level numerical representations. Currently, only decimals are +-- supported.+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Num.Reps (+ -- * Decimal representation+ --   $decdescription+ --  ** Digits+ D0, D1, D2, D3, D4, D5, D6, D7, D8, D9,+ --  ** Connective+ (:*)(..),+ ) where++import Data.Typeable (Typeable)+import Language.Haskell.TH.Syntax (Lift(..)) ++-------------------------+-- Decimal Representation+-------------------------++-- $decdescription +-- Decimals are represented using a different type (@Dx@) for each digit and a +-- binary infix connective (@:*@) to enable forming arbitrary precision +-- multidigit numbers. For example @D0@ represents number 0, @D4 :* D2@ +-- represents number 42, @D1 :* D0 :* D0@ represents 100, etc ... Obviously, +-- negative numbers cannot be represented.++-- | Decimal digit zero+data D0 deriving Typeable+instance Show D0 where show _ = "0"+instance Lift D0 where lift _ = [| undefined :: D0 |]+-- | Decimal digit one+data D1 deriving Typeable+instance Show D1 where show _ = "1"+instance Lift D1 where lift _ = [| undefined :: D1 |]+-- | Decimal digit two+data D2 deriving Typeable+instance Show D2 where show _ = "2"+instance Lift D2 where lift _ = [| undefined :: D2 |]+-- | Decimal digit three +data D3 deriving Typeable+instance Show D3 where show _ = "3"+instance Lift D3 where lift _ = [| undefined :: D3 |]+-- | Decimal digit four +data D4 deriving Typeable+instance Show D4 where show _ = "4"+instance Lift D4 where lift _ = [| undefined :: D4 |]+-- | Decimal digit five+data D5 deriving Typeable+instance Show D5 where show _ = "5"+instance Lift D5 where lift _ = [| undefined :: D5 |]+-- | Decimal digit six+data D6 deriving Typeable+instance Lift D6 where lift _ = [| undefined :: D6 |]+instance Show D6 where show _ = "6"+-- | Decimal digit seven+data D7 deriving Typeable+instance Show D7 where show _ = "7"+instance Lift D7 where lift _ = [| undefined :: D7 |]+-- | Decimal digit eight+data D8 deriving Typeable+instance Show D8 where show _ = "8"+instance Lift D8 where lift _ = [| undefined :: D8 |]+-- | Decimal digit nine+data D9 deriving Typeable+instance Show D9 where show _ = "9"+instance Lift D9 where lift _ = [| undefined :: D9 |]++-- | Connective to glue digits together.+--   For example, @D1 :* D0 :* D0@ represents the decimal number 100+data a :* b = a :* b deriving Typeable++instance (Show a, Show b) => Show (a :* b) where+  show _ = (show (undefined :: a)) ++ (show (undefined :: b))++instance (Lift a, Lift b) => Lift (a :* b) where+  lift _ = [| $(lift (undefined ::a)) :* $(lift (undefined :: b) ) |]
+ src/Data/TypeLevel/Num/Sets.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,+             UndecidableInstances, PatternSignatures, ScopedTypeVariables,+             Rank2Types #-}+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-name-shadowing #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.TypeLevel.Num.Sets+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+--                    and KTH's SAM group +-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  alfonso.acosta@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (non-standard instances)+--+-- Type-level numerical sets. Currently there is only support for Naturals and +-- Positives.+-- +----------------------------------------------------------------------------+module Data.TypeLevel.Num.Sets (Pos, Nat, toNum, toInt, reifyIntegral) where ++import Data.TypeLevel.Num.Reps++-----------+-- Naturals+-----------+++-- The well-formedness condition, the kind predicate.+-- These classes are internal, denoted by the ending "I", which is removed in +-- the exported proxies (read below)++-- | Naturals (Positives and zero), internal version+class NatI n where + -- | Reflecting function+ toNum :: Num a => n -> a+++-- | Less generic reflecting function (Int)+toInt :: Nat n => n -> Int+toInt =  toNum++++-- | Positives (Naturals without zero), internal version+class NatI n => PosI n++-- To prevent the user from adding new instances to NatI and especially+-- to PosI (e.g., to prevent the user from adding the instance |Pos D0|)+-- we do NOT export NatI and PosI. Rather, we export the following proxies.+-- The proxies entail PosI and NatI and so can be used to add PosI and NatI+-- constraints in the signatures. However, all the constraints below+-- are expressed in terms of NatI and PosI rather than proxies. Thus,+-- even if the user adds new instances to proxies, it would not matter.+-- Besides, because the following proxy instances are most general,+-- one may not add further instances without overlapping instance extension.++-- | Naturals (Positives and zero)+class    NatI n => Nat n+instance NatI n => Nat n++-- | Positives (Naturals without zero)+class    PosI n => Pos n+instance PosI n => Pos n++--------------------+-- Natural Instances+--------------------++-- Note: TH would be helpful to sistematically define instances +--       (our type level operations)+--       However, type-splicing is not yet implemented in GHC :S++-- monodigit naturals+instance NatI D0 where toNum _ = fromInteger 0+instance NatI D1 where toNum _ = fromInteger 1+instance NatI D2 where toNum _ = fromInteger 2+instance NatI D3 where toNum _ = fromInteger 3+instance NatI D4 where toNum _ = fromInteger 4+instance NatI D5 where toNum _ = fromInteger 5+instance NatI D6 where toNum _ = fromInteger 6+instance NatI D7 where toNum _ = fromInteger 7+instance NatI D8 where toNum _ = fromInteger 8+instance NatI D9 where toNum _ = fromInteger 9++-- multidigit naturals+-- Note: The PosI constraint guarantees that all valid representations are +-- normalized (i.e. D0 :* D1 will lead to a compiler error)+-- Note as well that ill-formed representations such as+-- (D1 :* D2) :* (D3 :* D4) are not recognized as instances of+-- naturals nor positives.+instance PosI x => NatI (x :* D0) where toNum n = subLastDec n+instance PosI x => NatI (x :* D1) where toNum n = subLastDec n + fromInteger 1+instance PosI x => NatI (x :* D2) where toNum n = subLastDec n + fromInteger 2+instance PosI x => NatI (x :* D3) where toNum n = subLastDec n + fromInteger 3+instance PosI x => NatI (x :* D4) where toNum n = subLastDec n + fromInteger 4+instance PosI x => NatI (x :* D5) where toNum n = subLastDec n + fromInteger 5+instance PosI x => NatI (x :* D6) where toNum n = subLastDec n + fromInteger 6+instance PosI x => NatI (x :* D7) where toNum n = subLastDec n + fromInteger 7+instance PosI x => NatI (x :* D8) where toNum n = subLastDec n + fromInteger 8+instance PosI x => NatI (x :* D9) where toNum n = subLastDec n + fromInteger 9++-- monodigit positives+instance PosI D1+instance PosI D2+instance PosI D3+instance PosI D4+instance PosI D5+instance PosI D6+instance PosI D7+instance PosI D8+instance PosI D9++-- multidigit positives+-- Note: The PosI constraint guarantees that all valid representations are +-- normalized (i.e. D0 :* D1 will lead to a compiler error)+instance PosI x => PosI (x :* D0)+instance PosI x => PosI (x :* D1)+instance PosI x => PosI (x :* D2)+instance PosI x => PosI (x :* D3)+instance PosI x => PosI (x :* D4)+instance PosI x => PosI (x :* D5)+instance PosI x => PosI (x :* D6)+instance PosI x => PosI (x :* D7)+instance PosI x => PosI (x :* D8)+instance PosI x => PosI (x :* D9)+++-- | Reification function. In CPS style (best possible solution)+reifyIntegral :: Integral i => i -> (forall n . Nat n => n -> r) -> r+reifyIntegral i f + | i < 0     = error "reifyIntegral: integral < 0"+ | i == 0    = f (undefined :: D0)+ | otherwise = reifyIntegralp i f +       -- reifyIntegral for positives+ where reifyIntegralp :: Integral i => i -> (forall n . Pos n => n -> r) -> r+       reifyIntegralp i f +         | i < 10 = case i of+                     1 -> f (undefined :: D1)+                     2 -> f (undefined :: D2); 3 -> f (undefined :: D3)+                     4 -> f (undefined :: D4); 5 -> f (undefined :: D5)+                     6 -> f (undefined :: D6); 7 -> f (undefined :: D7)+                     8 -> f (undefined :: D8); 9 -> f (undefined :: D9)+         | otherwise =  +            case m of+              0 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D0)) +              1 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D1))+              2 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D2))+              3 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D3))+              4 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D4))+              5 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D5))+              6 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D6))+              7 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D7))+              8 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D8))+              9 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D9))      +           where (d,m) = divMod i 10+++---------------------+-- Internal functions+---------------------++-- substract the last digit of a decimal type-level numeral and obtain +-- the result's reflected value +{-# INLINE subLastDec #-}+subLastDec :: (Num a, NatI (x :* d), NatI x) => x :* d -> a+subLastDec = (10*).toNum.div10Dec++-- Divide a decimal type-level numeral by 10 +{-# INLINE div10Dec #-} +div10Dec :: NatI (x :* d) => x :* d -> x+div10Dec _ = undefined
+ type-level.cabal view
@@ -0,0 +1,51 @@+name:           type-level+version:        0.1+cabal-version:  >= 1.2+build-type:     Simple+license:        BSD3+license-file:   LICENSE+copyright:      + Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+                    and KTH's SAM group+author:         Alfonso Acosta+maintainer:     alfonso.acosta@gmail.com+homepage:       http://code.haskell.org/type-level+stability:      alpha+package-url:    http://code.haskell.org/type-level+synopsis:       Type-level programming library+description:++ This library permits performing computations on the type-level. Type-level + functions are implemented using functional dependencies of multi+ parameter type classes. ++ To date, Booleans and Numerals (Naturals and Positives) are+ supported. With regard to Numerals, there is support for common+ arithmetic operations (addition, substraction, multiplication,+ division, exponientation, logarithm, maximum, comparison, GCD) + over natural numbers (using a decimal representation to make + compile-time errors friendlier).++ Although making use of type-level computations might seem devious and+ obfuscated at first sight, it is indeed useful in practice to implement + lightweight dependent types such us number-parameterized types (e.g. an array + type parameterized by the array's size or a modular group type Zn + parameterized by the modulus).++category:       Data+tested-with:    GHC==6.8.2+++-- depends on ghc due to the use of infix type constructors and template haskell+Library+  build-depends:   base, ghc, template-haskell > 2.0+  hs-source-dirs:  src+  exposed-modules: Data.TypeLevel,+                   Data.TypeLevel.Bool,+                   Data.TypeLevel.Num,+                   Data.TypeLevel.Num.Reps,+                   Data.TypeLevel.Num.Aliases,+                   Data.TypeLevel.Num.Sets,+                   Data.TypeLevel.Num.Ops,+                   Data.TypeLevel.Num.Aliases.TH+  ghc-options:	-Wall -O2