<h2 style="font-weight: normal;"><font size="2">Hi All,</font></h2><h2 style="font-weight: normal;"><font size="2">Inspired by Oleg's "Eliminating Array Bound Checking through Non-dependent types" </font><font size="2">
<a href="http://okmij.org/ftp/Haskell/types.html#branding">http://okmij.org/ftp/Haskell/types.html#branding</a>,</font></h2>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.
<br><br>In Oleg's examples with vectors he types in by hand the data whose type represents the size of the vector:<br><br>sample_v = listVec (D2 Sz) [True,False]<br><br>where (D2 Sz) is the size of the vector and the type is:
<br><br>ArbPrecDecT> :t sample_v<br>Vec (D2 Sz) Bool<br><br>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.<br><br>
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<br>int2typelevel :: (HList l) :: [Int] -> l<br><br>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.
<br><br>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.<br><br>Here is an example of what I want to be able to do:
<br><br>add :: Equal size1 size2 => Array size1 idx -> Array size2 idx -> Array size1 idx<br><br>for example:<br><br>data Array size idx = Array size (MArray idx Double)<br><br>add (Array (DCons (D1 (D2 Sz)) (DCons (D3 Sz) DNil)) (12,3)) (Array (DCons (D1 (D2 Sz)) (DCons (D3 Sz) DNil)) (12,3))
<br><br>the sizes are statically checked and I don't have to do runtime checking on the idx.<br><br>This message is a literate source file. The commented out function at the end illustrates the problem.<br><br>Thanks,
<br><br>Vivian<br><br>>{-# OPTIONS -fglasgow-exts #-}<br>><br>>-- copied from <a href="http://okmij.org/ftp/Haskell/number-parameterized-types.html">http://okmij.org/ftp/Haskell/number-parameterized-types.html</a>
<br>><br>>module Digits where<br>><br>>data D0 a = D0 a deriving(Eq,Read,Show)<br>>data D1 a = D1 a deriving(Eq,Read,Show)<br>>data D2 a = D2 a deriving(Eq,Read,Show)<br>>data D3 a = D3 a deriving(Eq,Read,Show)
<br>>data D4 a = D4 a deriving(Eq,Read,Show)<br>>data D5 a = D5 a deriving(Eq,Read,Show)<br>>data D6 a = D6 a deriving(Eq,Read,Show)<br>>data D7 a = D7 a deriving(Eq,Read,Show)<br>>data D8 a = D8 a deriving(Eq,Read,Show)
<br>>data D9 a = D9 a deriving(Eq,Read,Show)<br>><br>>class Digits ds where -- class of digit sequences<br>> ds2num:: (Num a) => ds -> a -> a -- CPS style<br>> <br>>data Sz = Sz -- zero size (or the Nil of the sequence)
<br>> deriving(Eq,Read,Show)<br>><br>>instance Digits Sz where<br>> ds2num _ acc = acc<br>> <br>>instance (Digits ds) => Digits (D0 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc)
<br>>instance (Digits ds) => Digits (D1 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 1)<br>>instance (Digits ds) => Digits (D2 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 2)
<br>>instance (Digits ds) => Digits (D3 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 3)<br>>instance (Digits ds) => Digits (D4 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 4)
<br>>instance (Digits ds) => Digits (D5 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 5)<br>>instance (Digits ds) => Digits (D6 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 6)
<br>>instance (Digits ds) => Digits (D7 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 7)<br>>instance (Digits ds) => Digits (D8 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 8)
<br>>instance (Digits ds) => Digits (D9 ds) where<br>> ds2num dds acc = ds2num (t22 dds) (10*acc + 9)<br>> <br>>t22::(f x) -> x; t22 = undefined<br>><br>>-- Class of non-negative numbers<br>>-- This is a restriction on Digits. It is not possible to make
<br>>-- such a restriction in SML.<br>>class {- (Digits c) => -} Card c where<br>> c2num:: (Num a) => c -> a<br>> <br>>instance Card Sz where c2num c = ds2num c 0<br>>--instance (NonZeroDigit d,Digits (d ds)) => Card (Sz (d ds)) where
<br>>instance (Digits ds) => Card (D1 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D2 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D3 ds) where c2num c = ds2num c 0
<br>>instance (Digits ds) => Card (D4 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D5 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D6 ds) where c2num c = ds2num c 0
<br>>instance (Digits ds) => Card (D7 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D8 ds) where c2num c = ds2num c 0<br>>instance (Digits ds) => Card (D9 ds) where c2num c = ds2num c 0
<br>><br>>-- Support for "generic" cards<br>>-- We introduce a data constructor CardC_unused merely for the sake of<br>>-- Haskell98. With the GHC extension, we can simply omit the data<br>>-- constructor and keep the type CardC purely abstract and phantom.
<br>>data CardC c1 c2 = CardC_unused<br>><br>>cardc:: (Card c1, Card c2) => c1 -> c2 -> CardC c1 c2<br>>cardc = undefined<br>>cardc1::CardC c1 c2 -> c1; cardc1 = undefined<br>>cardc2::CardC c1 c2 -> c2; cardc2 = undefined
<br>><br>>instance (Card c1, Card c2) => Card (CardC c1 c2) where<br>> c2num c12 = c2num (cardc1 c12) + c2num (cardc2 c12)<br>><br>>-----------------------------------------------------------------------------
<br>>-- make lists<br>><br>>-- copied from HList: <a href="http://okmij.org/ftp/Haskell/types.html#HList">http://okmij.org/ftp/Haskell/types.html#HList</a><br>><br>>data DNil = DNil deriving (Eq,Show,Read)
<br>>data DCons e l = DCons e l deriving (Eq,Show,Read)<br>><br>>class DList l<br>>instance DList DNil<br>>instance (Digits e, DList l) => DList (DCons e l)<br>><br>>dNil :: DNil<br>>dNil = DNil
<br>><br>>dCons :: forall e. Digits e => (DList l => e -> l -> DCons e l)<br>>dCons e l = DCons e l<br>><br>>-- ^ Oleg<br>>-----------------------------------------------------------------------------
<br>>-- v Vivian<br>><br>>-- CPS<br>>num2digits :: (Integral a, Show a) => a -> (forall ds. (Digits ds) => ds -> o) -> o<br>>num2digits n = str2digits (show n) <br>><br>>str2digits :: String -> (forall ds. (Digits ds) => ds -> o) -> o
<br>>str2digits [] k = k Sz<br>>str2digits ('0' : ss) k = str2digits ss (\ds -> k (D0 ds))<br>>str2digits ('1' : ss) k = str2digits ss (\ds -> k (D1 ds))<br>>str2digits ('2' : ss) k = str2digits ss (\ds -> k (D2 ds))
<br>>str2digits ('3' : ss) k = str2digits ss (\ds -> k (D3 ds))<br>>str2digits ('4' : ss) k = str2digits ss (\ds -> k (D4 ds))<br>>str2digits ('5' : ss) k = str2digits ss (\ds -> k (D5 ds))
<br>>str2digits ('6' : ss) k = str2digits ss (\ds -> k (D6 ds))<br>>str2digits ('7' : ss) k = str2digits ss (\ds -> k (D7 ds))<br>>str2digits ('8' : ss) k = str2digits ss (\ds -> k (D8 ds))
<br>>str2digits ('9' : ss) k = str2digits ss (\ds -> k (D9 ds))<br>><br>>-----------------------------------------------------------------------------<br>><br>>--test = num2str 10 (\x -> dCons x dNil)
<br><br>