type-level-tf (empty) → 0.2.1
raw patch · 11 files changed
+1478/−0 lines, 11 filesdep +basedep +sybdep +template-haskellsetup-changed
Dependencies added: base, syb, template-haskell
Files
- LICENSE +26/−0
- Setup.hs +7/−0
- src/Data/TypeLevel.hs +20/−0
- src/Data/TypeLevel/Bool.hs +191/−0
- src/Data/TypeLevel/Num.hs +25/−0
- src/Data/TypeLevel/Num/Aliases.hs +29/−0
- src/Data/TypeLevel/Num/Aliases/TH.hs +130/−0
- src/Data/TypeLevel/Num/Ops.hs +734/−0
- src/Data/TypeLevel/Num/Reps.hs +91/−0
- src/Data/TypeLevel/Num/Sets.hs +172/−0
- type-level-tf.cabal +53/−0
+ 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.
+ 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 src/Data/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,191 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies,+ Rank2Types, DeriveDataTypeable, FlexibleInstances,+ UndecidableInstances, FlexibleContexts,ScopedTypeVariables,+ TypeFamilies+ #-}+-----------------------------------------------------------------------------+-- |+-- Module : Data.TypeLevel.Bool+-- Copyright : (c) 2008 Benedikt Huber (port to Associative types (ghc 6.9+)) +-- (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, toBool,+ False, false,+ True, true,+ -- reifyBool,+ -- * Type-level boolean operations+ Not,+ And,+ Or+ -- Not, not,+ -- And, (&&),+ -- Or, (||),+ -- Xor, xor,+ -- Impl, imp,+) 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++type family And b_0 b_1+type instance And True True = True+type instance And True False = False+type instance And False True = False+type instance And False False = False++type family Or b_0 b_1+type instance Or True True = True+type instance Or True False = True+type instance Or False True = True+type instance Or False False = False++type family Not b+type instance Not True = False+type instance Not False = True++#if 0+type family Id b+type family Const a b+type instance Id a = a+type instance Const b a = b+-- | Booleans, internal version+class BoolI b where+ toBool :: b -> P.Bool+ type Not b+ type And b :: * -> *+ type Or b :: * -> *+ type Xor b :: * -> *+ type Impl b :: * -> *+ type BoolEq b :: * -> *++-- 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+ type Not True = False+ type And True = Id+ type Or True = Const True+ type Xor True = Not+ type Impl True = Id+ type BoolEq True = Id+ +instance BoolI False where+ toBool _ = False+ type Not False = True+ type And False = Const False+ type Or False = Id+ type Xor False = Id+ type Impl False = Const True+ type BoolEq False = Not+-- | 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+-------------+++-- | value-level reflection function for the 'Not' type-level relation+not :: b1 -> Not b1+not = undefined++-- | 'And' type-level relation. @And b1 b2 b3@ establishes that+-- @b1 && b2 = b3@+++-- | value-level reflection function for the 'And' type-level relation+(&&) :: b1 -> b2 -> And b1 b2+(&&) = undefined+infixr 3 &&+ +-- | Or type-level relation. @Or b1 b2 b3@ establishes that+-- @b1 || b2 = b3@+++-- | value-level reflection function for the 'Or' type-level relation+(||) :: b1 -> b2 -> Or b1 b2+(||) = undefined+infixr 2 ||++-- | Exclusive or type-level relation. @Xor b1 b2 b3@ establishes that+-- @xor b1 b2 = b3@++-- | value-level reflection function for the 'Xor' type-level relation+xor :: b1 -> b2 -> Xor b1 b2+xor = undefined+++-- | Implication type-level relation. @Imp b1 b2 b3@ establishes that+-- @b1 =>b2 = b3@++-- | value-level reflection function for the Imp type-level relation+imp :: b1 -> b2 -> Impl b1 b2+imp = undefined+++-- Although equality can be defined as the composition of Xor and Not+-- we define it specifically++-- | Boolean equality type-level relation++-- 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+boolEq :: b1 -> b2 -> BoolEq b1 b2+boolEq = undefined+#endif+
+ 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,734 @@+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeOperators,+ FlexibleInstances, FlexibleContexts, UndecidableInstances,+ EmptyDataDecls, TypeFamilies #-}+-----------------------------------------------------------------------------+-- |+-- 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, (^),+ -- Not implemented+ -- 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,+ OrderingEq, NatEq,+ -- ** 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@.+-- Assoc notes: Cannot avoid malformed types+type family Succ n+type instance Succ D0 = D1+type instance Succ D1 = D2+type instance Succ D2 = D3+type instance Succ D3 = D4+type instance Succ D4 = D5+type instance Succ D5 = D6+type instance Succ D6 = D7+type instance Succ D7 = D8+type instance Succ D8 = D9+type instance Succ D9 = (D1 :* D0)+type instance Succ (x:*D0) = (x:*D1)+type instance Succ (x:*D1) = (x:*D2)+type instance Succ (x:*D2) = (x:*D3)+type instance Succ (x:*D3) = (x:*D4)+type instance Succ (x:*D4) = (x:*D5)+type instance Succ (x:*D5) = (x:*D6)+type instance Succ (x:*D6) = (x:*D7)+type instance Succ (x:*D7) = (x:*D8)+type instance Succ (x:*D8) = (x:*D9)+type instance Succ (x:*D9) = (Succ x:*D0)+++++-- | value-level reflection function for the 'Succ' type-level relation+succ :: x -> Succ x+succ = undefined++type family Pred n+type instance Pred D1 = D0+type instance Pred D2 = D1+type instance Pred D3 = D2+type instance Pred D4 = D3+type instance Pred D5 = D4+type instance Pred D6 = D5+type instance Pred D7 = D6+type instance Pred D8 = D7+type instance Pred D9 = D8+type instance Pred (D1:*D0) = D9+type instance Pred (D2:*D0) = (D1:*D9)+type instance Pred (D3:*D0) = (D2:*D9)+type instance Pred (D4:*D0) = (D3:*D9)+type instance Pred (D5:*D0) = (D4:*D9)+type instance Pred (D6:*D0) = (D5:*D9)+type instance Pred (D7:*D0) = (D6:*D9)+type instance Pred (D8:*D0) = (D7:*D9)+type instance Pred (D9:*D0) = (D8:*D9)+type instance Pred (xd:*xm:*D0) = Pred(xd:*xm):*D9+type instance Pred (xd:*D1) = (xd:*D0)+type instance Pred (xd:*D2) = (xd:*D1)+type instance Pred (xd:*D3) = (xd:*D2)+type instance Pred (xd:*D4) = (xd:*D3)+type instance Pred (xd:*D5) = (xd:*D4)+type instance Pred (xd:*D6) = (xd:*D5)+type instance Pred (xd:*D7) = (xd:*D6)+type instance Pred (xd:*D8) = (xd:*D7)+type instance Pred (xd:*D9) = (xd:*D8)++pred :: x -> Pred x+pred = undefined++--+----------------------+---- Add and Subtract+----------------------+--+type family Div10 m +type instance Div10 D0 = D0+type instance Div10 D1 = D0+type instance Div10 D2 = D0+type instance Div10 D3 = D0+type instance Div10 D4 = D0+type instance Div10 D5 = D0+type instance Div10 D6 = D0+type instance Div10 D7 = D0+type instance Div10 D8 = D0+type instance Div10 D9 = D0+type instance Div10 (x:*D0) = x+type instance Div10 (x:*D1) = x+type instance Div10 (x:*D2) = x+type instance Div10 (x:*D3) = x+type instance Div10 (x:*D4) = x+type instance Div10 (x:*D5) = x+type instance Div10 (x:*D6) = x+type instance Div10 (x:*D7) = x+type instance Div10 (x:*D8) = x+type instance Div10 (x:*D9) = x+div10 :: x -> Div10 x+div10 = undefined++type family Mod10 n+type instance Mod10 D0 = D0+type instance Mod10 D1 = D1+type instance Mod10 D2 = D2+type instance Mod10 D3 = D3+type instance Mod10 D4 = D4+type instance Mod10 D5 = D5+type instance Mod10 D6 = D6+type instance Mod10 D7 = D7+type instance Mod10 D8 = D8+type instance Mod10 D9 = D9+type instance Mod10 (xd:*xm) = xm+mod10 :: x -> Mod10 x+mod10 = undefined++type family DivMod10 n+type instance DivMod10 n = (Div10 n, Mod10 n)++type family Add m n :: *+type instance Add D0 x = x+type instance Add D1 x = (Succ x)+type instance Add D2 x = Add D1 (Succ x)+type instance Add D3 x = Add D2 (Succ x)+type instance Add D4 x = Add D3 (Succ x)+type instance Add D5 x = Add D4 (Succ x)+type instance Add D6 x = Add D5 (Succ x)+type instance Add D7 x = Add D6 (Succ x)+type instance Add D8 x = Add D7 (Succ x)+type instance Add D9 x = Add D8 (Succ x)+type instance Add (xd :* xm) y = Add xm ((Add xd (Div10 y)) :* (Mod10 y))+++-- | value-level reflection function for the 'Add' type-level relation +(+) :: x -> y -> Add x y+(+) = undefined+++-- --| Subtraction type-level relation. @Sub x y z@ establishes+-- -- that @x - y = z@ +type family Sub x y+type instance Sub x D0 = x+type instance Sub x D1 = (Pred x) +type instance Sub x D2 = Sub (Pred x) D1+type instance Sub x D3 = Sub (Pred x) D2+type instance Sub x D4 = Sub (Pred x) D3+type instance Sub x D5 = Sub (Pred x) D4+type instance Sub x D6 = Sub (Pred x) D5+type instance Sub x D7 = Sub (Pred x) D6+type instance Sub x D8 = Sub (Pred x) D7+type instance Sub x D9 = Sub (Pred x) D8+type instance Sub x (xd :* xm) = Sub (Pred x) (Pred (xd:*xm))++-- | value-level reflection function for the 'Sub' type-level relation +(-) :: x -> y -> Sub x y+(-) = undefined+--+--------------------------------+---- Multiplication and Division+--------------------------------+--+-------------------+---- Multiplication+-------------------+--+---- | Multiplication type-level relation. @Mul x y z@ establishes+---- that @x * y = z@.+type family Mul m n+type instance Mul D0 y = D0+type instance Mul D1 y = y+type instance Mul D2 y = Add y y+type instance Mul D3 y = Add y (Mul D2 y)+type instance Mul D4 y = Add y (Mul D3 y)+type instance Mul D5 y = Add y (Mul D4 y)+type instance Mul D6 y = Add y (Mul D5 y)+type instance Mul D7 y = Add y (Mul D6 y)+type instance Mul D8 y = Add y (Mul D7 y)+type instance Mul D9 y = Add y (Mul D8 y)+-- Note that this is only valid if xd is positive.+type instance Mul (xd :* xm) y = Add (Mul xm y) ((Mul xd y) :* D0)++-- | value-level reflection function for the multiplication type-level relation +(*) :: x -> y -> Mul x y+(*) = undefined+++--+--+-------------+---- Division+-------------++-- | Division and Remainder type-level relation. @DivMod x y q r@ establishes+-- that @x/y = q + r/y@++-- division + modulo+-- x/y | y > x = (0,x)+-- x/y | y <= x = ( 1 + (x-y / y), mod (x - y))++-- This doesn't work+--type instance Div x y = Cond (y :>: x) D0 (Succ (Div (Sub x y) y))+--type instance Mod x y = Cond (y :>: x) x (Mod (Sub x y) y)++type family Div' x y x_gt_y+type instance Div' x y False = D0+type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y)) +type family Div x y+type instance Div x y = Div' x y (Trich x y)++type family Mod' x y x_gt_y+type instance Mod' x y False = x+type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :>=: y)+type family Mod x y+type instance Mod x y = Mod' x y (x :>=: y)+++-- | value-level reflection function for the 'DivMod' type-level relation+divMod :: x -> y -> (Div x y, Mod x y)+divMod _ _ = (undefined)++-- | value-level reflection function for the 'Div' type-level relation +div :: x -> y -> Div x y+div = undefined++-- | value-level reflection function for the 'Mod' type-level relation +mod :: x -> y -> Mod x y+mod = undefined+++------------------------------------------+---- Multiplication/Division special cases+------------------------------------------++-- | Multiplication by 10 type-level relation (based on 'DivMod10').+-- @Mul10 x y@ establishes that @10 * x = y@.+type family Mul10 n+type instance Mul10 x = (x :* D0)++-- | value-level reflection function for 'Mul10' +mul10 :: x -> Mul10 x+mul10 = undefined+++---- | value-level reflection function for DivMod10 +divMod10 :: x -> (Div10 x, Mod10 x)+divMod10 _ = (undefined, undefined)++--+------------------------------+---- Is-Divisible-By assertion+------------------------------++-- | Is-divisible-by type-level assertion. e.g @IsDivBy d x@ establishes that+-- @x@ is divisible by @d@.++-- here we use a class for demonstration purposes+class (Pos d, Nat x) => IsDivBy d x+instance (Pos d, Nat x, Mod x d ~ D0) => IsDivBy d x++-- | value-level reflection function for IsDivBy+isDivBy :: IsDivBy d x => d -> x -> ()+isDivBy _ _ = ()++-----------------------------+---- Exponentiation/Logarithm+-----------------------------+--+---- | Exponentation type-level relation. @ExpBase b e r@ establishes+---- that @b^e = r@+type family ExpBase b e+type instance ExpBase b D0 = D1+type instance ExpBase b D1 = b+type instance ExpBase b D2 = (Mul b b)+type instance ExpBase b D3 = (Mul b (ExpBase b D2))+type instance ExpBase b D4 = (Mul b (ExpBase b D3))+type instance ExpBase b D5 = (Mul b (ExpBase b D4))+type instance ExpBase b D6 = (Mul b (ExpBase b D5))+type instance ExpBase b D7 = (Mul b (ExpBase b D6))+type instance ExpBase b D8 = (Mul b (ExpBase b D7))+type instance ExpBase b D9 = (Mul b (ExpBase b D8))+type instance ExpBase b (ei :* el) = Mul b (ExpBase b (Pred (ei:* el)))++-- | value-level reflection function for the ExpBase type-level relation+(^) :: b -> e -> ExpBase b e+(^) = undefined++---------------- LEFT OUT FOR NOW ---------------------------------++-- 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+-------------------------------------++type family Exp10 x+type instance Exp10 D0 = D1+type instance Exp10 D1 = (D1 :* D0)+type instance Exp10 D2 = (D1 :* D0 :* D0)+type instance Exp10 D3 = (D1 :* D0 :* D0 :* D0)+type instance Exp10 D4 = (D1 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 D5 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 D6 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 D7 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 D8 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 D9 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)+type instance Exp10 (xi :* xl) = (Exp10 (Pred (xi:*xl)) :* D0)++-- | value-level reflection function for Exp10+exp10 :: x -> Exp10 x+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)+type family Log10 x +type instance Log10 D1 = D0+type instance Log10 D2 = D0+type instance Log10 D3 = D0+type instance Log10 D4 = D0+type instance Log10 D5 = D0+type instance Log10 D6 = D0+type instance Log10 D7 = D0+type instance Log10 D8 = D0+type instance Log10 D9 = D0+type instance Log10 (xi :* xl) = Pred (Log10 xi)++-- | value-level reflection function for 'Log10'+log10 :: x -> Log10 x+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++type family OrderingEq o1 o2+type instance OrderingEq LT LT = True+type instance OrderingEq LT EQ = False+type instance OrderingEq LT GT = False+type instance OrderingEq EQ EQ = True+type instance OrderingEq EQ LT = False+type instance OrderingEq EQ GT = False+type instance OrderingEq GT GT = True+type instance OrderingEq GT LT = False+type instance OrderingEq GT EQ = False++-- | 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@)+type family Trich x y++-- | value-level reflection function for the comparison type-level assertion +trich :: x -> y -> Trich x y+trich = undefined++-- by structural induction on the first, and then the second argument+-- D0+type instance Trich D0 D0 = EQ+type instance Trich D0 D1 = LT+type instance Trich D0 D2 = LT+type instance Trich D0 D3 = LT+type instance Trich D0 D4 = LT+type instance Trich D0 D5 = LT+type instance Trich D0 D6 = LT+type instance Trich D0 D7 = LT+type instance Trich D0 D8 = LT+type instance Trich D0 D9 = LT+type instance Trich D0 (yi :* yl) = LT+type instance Trich (yi :* yl) D0 = GT+-- D1+type instance Trich D1 D0 = GT+type instance Trich D1 D1 = EQ+type instance Trich D1 D2 = LT+type instance Trich D1 D3 = LT +type instance Trich D1 D4 = LT+type instance Trich D1 D5 = LT +type instance Trich D1 D6 = LT+type instance Trich D1 D7 = LT +type instance Trich D1 D8 = LT+type instance Trich D1 D9 = LT+type instance Trich D1 (yi :* yl) = LT+type instance Trich (yi :* yl) D1 = GT+-- D2+type instance Trich D2 D0 = GT+type instance Trich D2 D1 = GT+type instance Trich D2 D2 = EQ+type instance Trich D2 D3 = LT+type instance Trich D2 D4 = LT+type instance Trich D2 D5 = LT+type instance Trich D2 D6 = LT+type instance Trich D2 D7 = LT+type instance Trich D2 D8 = LT+type instance Trich D2 D9 = LT+type instance Trich D2 (yi :* yl) = LT+type instance Trich (yi :* yl) D2 = GT+-- D3+type instance Trich D3 D0 = GT+type instance Trich D3 D1 = GT+type instance Trich D3 D2 = GT+type instance Trich D3 D3 = EQ+type instance Trich D3 D4 = LT+type instance Trich D3 D5 = LT+type instance Trich D3 D6 = LT+type instance Trich D3 D7 = LT+type instance Trich D3 D8 = LT+type instance Trich D3 D9 = LT+type instance Trich D3 (yi :* yl) = LT+type instance Trich (yi :* yl) D3 = GT+-- D4+type instance Trich D4 D0 = GT+type instance Trich D4 D1 = GT+type instance Trich D4 D2 = GT+type instance Trich D4 D3 = GT+type instance Trich D4 D4 = EQ+type instance Trich D4 D5 = LT+type instance Trich D4 D6 = LT+type instance Trich D4 D7 = LT+type instance Trich D4 D8 = LT+type instance Trich D4 D9 = LT+type instance Trich D4 (yi :* yl) = LT+type instance Trich (yi :* yl) D4 = GT+-- D5+type instance Trich D5 D0 = GT+type instance Trich D5 D1 = GT+type instance Trich D5 D2 = GT+type instance Trich D5 D3 = GT+type instance Trich D5 D4 = GT+type instance Trich D5 D5 = EQ+type instance Trich D5 D6 = LT+type instance Trich D5 D7 = LT+type instance Trich D5 D8 = LT+type instance Trich D5 D9 = LT+type instance Trich D5 (yi :* yl) = LT+type instance Trich (yi :* yl) D5 = GT+-- D6+type instance Trich D6 D0 = GT+type instance Trich D6 D1 = GT+type instance Trich D6 D2 = GT+type instance Trich D6 D3 = GT+type instance Trich D6 D4 = GT+type instance Trich D6 D5 = GT+type instance Trich D6 D6 = EQ+type instance Trich D6 D7 = LT+type instance Trich D6 D8 = LT+type instance Trich D6 D9 = LT+type instance Trich D6 (yi :* yl) = LT+type instance Trich (yi :* yl) D6 = GT+-- D7+type instance Trich D7 D0 = GT+type instance Trich D7 D1 = GT+type instance Trich D7 D2 = GT+type instance Trich D7 D3 = GT+type instance Trich D7 D4 = GT+type instance Trich D7 D5 = GT+type instance Trich D7 D6 = GT+type instance Trich D7 D7 = EQ+type instance Trich D7 D8 = LT+type instance Trich D7 D9 = LT+type instance Trich D7 (yi :* yl) = LT+type instance Trich (yi :* yl) D7 = GT+-- D8+type instance Trich D8 D0 = GT+type instance Trich D8 D1 = GT+type instance Trich D8 D2 = GT+type instance Trich D8 D3 = GT+type instance Trich D8 D4 = GT+type instance Trich D8 D5 = GT+type instance Trich D8 D6 = GT+type instance Trich D8 D7 = GT+type instance Trich D8 D8 = EQ+type instance Trich D8 D9 = LT+type instance Trich D8 (yi :* yl) = LT+type instance Trich (yi :* yl) D8 = GT+-- D9+type instance Trich D9 D0 = GT+type instance Trich D9 D1 = GT+type instance Trich D9 D2 = GT+type instance Trich D9 D3 = GT+type instance Trich D9 D4 = GT+type instance Trich D9 D5 = GT+type instance Trich D9 D6 = GT+type instance Trich D9 D7 = GT+type instance Trich D9 D8 = GT+type instance Trich D9 D9 = EQ+type instance Trich D9 (yi :* yl) = LT+type instance Trich (yi :* yl) D9 = GT+++-- multidigit comparison+type instance Trich (xd :* xm) (yd :* ym) = CS (Trich xd yd) (Trich xm ym)++-- strengthen the comparison relation+type family CS c1 c2+type instance CS EQ r = r+type instance CS GT r = GT+type instance CS LT r = LT++-- Abbreviated comparison assertions++-- | Equality abbreviated type-level assertion+type family NatEq x y+type instance NatEq x y = OrderingEq (Trich x y) EQ++-- | Greater-than abbreviated type-level assertion+type family x :>: y+type instance x :>: y = OrderingEq (Trich x y) GT++-- | value-level reflection function for >+(>) :: x -> y -> x :>: y+(>) = undefined++-- | Lower-than abbreviated type-level assertion+type family x :<: y+type instance x :<: y = OrderingEq (Trich x y) LT++-- | value-level reflection function for >+(<) :: x -> y -> x :<: y+(<) = undefined++-- | Greater-than or equal abbreviated type-level assertion+type family x :>=: y+type instance x :>=: y = (Succ x) :>: y++-- | value-level reflection function for >=+(>=) :: x -> y -> x :>=: y+(>=) = undefined++-- | Less-than or equal abbreviated type-level assertion+type family x :<=: y+type instance x :<=: y = x :<: (Succ y)++-- | value-level reflection function for >=+(<=) :: x -> y -> x :<=: y+(<=) = undefined+++--------------------+---- Maximum/Minimum+--------------------+type family Max x y+type instance Max x y = Cond (x :>: y) x y+type family Min x y+type instance Min x y = Cond (x :<=: y) x y++-- | value-level reflection function for the maximum type-level relation+max :: x -> y -> Max x y+max = undefined++-- | value-level reflection function for the minimum type-level relation+min :: x -> y -> Min x y+min = undefined++---------+---- GCD+---------++-- | Greatest Common Divisor type-level relation+type family GCD x y+type instance GCD x y = GCD' x y (IsZero y) (Trich x y)++---- Euclidean algorithm +--class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd+type family GCD' x y ys cmp+type instance GCD' x D0 True cmp = D0+type instance GCD' x y False LT = GCD y x+type instance GCD' x y False EQ = x+type instance GCD' x y False GT = GCD (Sub x y) y++-- | value-level reflection function for the GCD type-level relation+gcd :: x -> y -> GCD x y+gcd = undefined++-----------------------+---- Internal functions+-----------------------+--+-- classify a natural as positive or zero+type family IsZero n+type instance IsZero D0 = True+type instance IsZero D1 = False+type instance IsZero D2 = False+type instance IsZero D3 = False+type instance IsZero D4 = False+type instance IsZero D5 = False+type instance IsZero D6 = False+type instance IsZero D7 = False+type instance IsZero D8 = False+type instance IsZero D9 = False+-- debatable+type instance IsZero (xd:*xm) = And (IsZero xd) (IsZero xm)++-- +-- The cond TF+type family Cond b x y+type instance Cond True x y = x+type instance Cond False x y = y+
+ src/Data/TypeLevel/Num/Reps.hs view
@@ -0,0 +1,91 @@+{-# 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.List+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, 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-tf.cabal view
@@ -0,0 +1,53 @@+name: type-level-tf+version: 0.2.1+license: BSD3+license-file: LICENSE+copyright: + Copyright (c) 2010 Corey O'Connor+ Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch+ and KTH's SAM group+ 2008 Benedikt Huber (Rewrite using type families)+author: Corey O'Connor, Alfonso Acosta+homepage: https://github.com/coreyoconnor/type-level-tf+maintainer: coreyoconnor@gmail.com+stability: alpha+synopsis: Type-level programming library (type families)+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.9.0, GHC==6.12.0, GHC==7.2.1+cabal-version: >= 1.6+build-type: Simple++source-repository head+ type: git+ location: git://github.com/coreyoconnor/type-level-tf.git++Library+ build-depends: base == 4.*, template-haskell > 2.0, syb+ 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