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)