[Haskell-cafe] Type level programming to eliminate array bound checking, a real world use

[Vivian McPhail]

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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070411/d15c3ec4/attachment-0001.htm