Hi All,Inspired by Oleg's "Eliminating Array Bound Checking through
Non-dependent types" http://okmij.org/ftp/Haskell/types.html#branding,I am
attempting to write code that will receive an array from C land and convert
it to a type safe representation. The array could have n dimensions where n
2. I receive the number of dimensions as a list of Ints [Int]. To do
type-safe programming I need to convert this to a type level
representation. Using CPS (thanks to ski on #haskell) I can convert an Int
to the type level. But I have found it impossible to insert this type-level
Digits representation into an HList.
In Oleg's examples with vectors he types in by hand the data whose type
represents the size of the vector:
sample_v = listVec (D2 Sz) [True,False]
where (D2 Sz) is the size of the vector and the type is:
ArbPrecDecT> :t sample_v
Vec (D2 Sz) Bool
In a real program we can't expect the programmer to type in the size of the
data, it needs to be done programmatically, and this is where I am stuck.
Could someone please point me in the right direction, or explain why what
I'm trying to do won't work? Basically I'm looking for a function
int2typelevel :: (HList l) :: [Int] -> l
I thought that this would work because HLists can have elements of different
types and I can already (modulo CPS) convert an Int to it's Digits type
level representation.
One approach which won't work is existentially wrapping the result of
num2digits in a GADT, because this hides the type from the type-checker and
then can't be used for bounds checking.
Here is an example of what I want to be able to do:
add :: Equal size1 size2 => Array size1 idx -> Array size2 idx -> Array
size1 idx
for example:
data Array size idx = Array size (MArray idx Double)
add (Array (DCons (D1 (D2 Sz)) (DCons (D3 Sz) DNil)) (12,3)) (Array (DCons
(D1 (D2 Sz)) (DCons (D3 Sz) DNil)) (12,3))
the sizes are statically checked and I don't have to do runtime checking on
the idx.
This message is a literate source file. The commented out function at the
end illustrates the problem.
Thanks,
Vivian
{-# OPTIONS -fglasgow-exts #-}
-- copied from http://okmij.org/ftp/Haskell/number-parameterized-types.html
module Digits where
data D0 a = D0 a deriving(Eq,Read,Show)
data D1 a = D1 a deriving(Eq,Read,Show)
data D2 a = D2 a deriving(Eq,Read,Show)
data D3 a = D3 a deriving(Eq,Read,Show)
data D4 a = D4 a deriving(Eq,Read,Show)
data D5 a = D5 a deriving(Eq,Read,Show)
data D6 a = D6 a deriving(Eq,Read,Show)
data D7 a = D7 a deriving(Eq,Read,Show)
data D8 a = D8 a deriving(Eq,Read,Show)
data D9 a = D9 a deriving(Eq,Read,Show)
class Digits ds where -- class of digit sequences
ds2num:: (Num a) => ds -> a -> a -- CPS style
data Sz = Sz -- zero size (or the Nil of the sequence)
deriving(Eq,Read,Show)
instance Digits Sz where
ds2num _ acc = acc
instance (Digits ds) => Digits (D0 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc)
instance (Digits ds) => Digits (D1 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 1)
instance (Digits ds) => Digits (D2 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 2)
instance (Digits ds) => Digits (D3 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 3)
instance (Digits ds) => Digits (D4 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 4)
instance (Digits ds) => Digits (D5 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 5)
instance (Digits ds) => Digits (D6 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 6)
instance (Digits ds) => Digits (D7 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 7)
instance (Digits ds) => Digits (D8 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 8)
instance (Digits ds) => Digits (D9 ds) where
ds2num dds acc = ds2num (t22 dds) (10*acc + 9)
t22::(f x) -> x; t22 = undefined
-- Class of non-negative numbers
-- This is a restriction on Digits. It is not possible to make
-- such a restriction in SML.
class {- (Digits c) => -} Card c where
c2num:: (Num a) => c -> a
instance Card Sz where c2num c = ds2num c 0
--instance (NonZeroDigit d,Digits (d ds)) => Card (Sz (d ds)) where
instance (Digits ds) => Card (D1 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D2 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D3 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D4 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D5 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D6 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D7 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D8 ds) where c2num c = ds2num c 0
instance (Digits ds) => Card (D9 ds) where c2num c = ds2num c 0
-- Support for "generic" cards
-- We introduce a data constructor CardC_unused merely for the sake of
-- Haskell98. With the GHC extension, we can simply omit the data
-- constructor and keep the type CardC purely abstract and phantom.
data CardC c1 c2 = CardC_unused
cardc:: (Card c1, Card c2) => c1 -> c2 -> CardC c1 c2
cardc = undefined
cardc1::CardC c1 c2 -> c1; cardc1 = undefined
cardc2::CardC c1 c2 -> c2; cardc2 = undefined
instance (Card c1, Card c2) => Card (CardC c1 c2) where
c2num c12 = c2num (cardc1 c12) + c2num (cardc2 c12)
-----------------------------------------------------------------------------
-- make lists
-- copied from HList: http://okmij.org/ftp/Haskell/types.html#HList
data DNil = DNil deriving (Eq,Show,Read)
data DCons e l = DCons e l deriving (Eq,Show,Read)
class DList l
instance DList DNil
instance (Digits e, DList l) => DList (DCons e l)
dNil :: DNil
dNil = DNil
dCons :: forall e. Digits e => (DList l => e -> l -> DCons e l)
dCons e l = DCons e l
-- ^ Oleg
-----------------------------------------------------------------------------
-- v Vivian
-- CPS
num2digits :: (Integral a, Show a) => a -> (forall ds. (Digits ds) => ds ->
o) -> o
num2digits n = str2digits (show n)
str2digits :: String -> (forall ds. (Digits ds) => ds -> o) -> o
str2digits [] k = k Sz
str2digits ('0' : ss) k = str2digits ss (\ds -> k (D0 ds))
str2digits ('1' : ss) k = str2digits ss (\ds -> k (D1 ds))
str2digits ('2' : ss) k = str2digits ss (\ds -> k (D2 ds))
str2digits ('3' : ss) k = str2digits ss (\ds -> k (D3 ds))
str2digits ('4' : ss) k = str2digits ss (\ds -> k (D4 ds))
str2digits ('5' : ss) k = str2digits ss (\ds -> k (D5 ds))
str2digits ('6' : ss) k = str2digits ss (\ds -> k (D6 ds))
str2digits ('7' : ss) k = str2digits ss (\ds -> k (D7 ds))
str2digits ('8' : ss) k = str2digits ss (\ds -> k (D8 ds))
str2digits ('9' : ss) k = str2digits ss (\ds -> k (D9 ds))
-----------------------------------------------------------------------------
--test = num2str 10 (\x -> dCons x dNil)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
