Параметризиране на типове чрез цели числа в Haskell

Опитвам се да направя някои типове на Haskell, които са параметризирани не от типове, а от елементи от тип, по-специално цели числа. Например (линейно-алгебра) вектор в R^2 и вектор в R^3 са различни типизирани обекти. По-конкретно, пиша K-D дърво в Haskell и искам да параметризирам моята структура от данни чрез положително цяло число, така че 3-D дърво и 4-D дърво да имат различен тип.

Опитах се да параметризирам дървото си чрез кортежи, но не изглеждаше да върви никъде (и изглежда малко вероятно това да може да бъде прокарано, особено след като не изглежда, че тройките или нещо по-голямо дори са функтори (и Не знам по никакъв начин да кажа като например HomogeneousTuple a => Functor a). Искам да направя нещо подобно:

data (TupleOfDoubles a) => KDTree a b = ... ---so in a 3DTree a is (Double,Double,Double)

това би било хубаво или нещо подобно би било също толкова добро

data KDTree Int a = ... -- The Int is k, so KDTree has kind Int -> * -> *

Някой знае ли дали някой от тези ефекти е работещ или разумен?

Благодаря - Джоузеф


haskell algebraic-data-types kdtree higher-kinded-types
person Joseph Victor    schedule 01.09.2011    source източник
comment
странична бележка, може да се интересувате от част от литературата за зависими типове, което е по-общ вид функции от стойности до типове: хареса ми cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf   -  person Amos Robinson    schedule 01.09.2011
comment
благодаря, Амос, това изглежда нещо, което мога да използвам   -  person Joseph Victor    schedule 01.09.2011

Отговори (2)


arrow_upward
5
arrow_downward

Има GHC разширение, върху което се работи, наречено TypeNats, което би било точно това, което искате. Въпреки това крайъгълният камък за това в момента е зададен да бъде 7.4.1 според тикета, така че това ще изчакайте още малко.

Докато това разширение не е налично, единственото нещо, което можете да направите, е да кодирате измерението с помощта на типове. Например нещо по този начин може да работи:

{-# LANGUAGE ScopedTypeVariables #-}
class MyTypeNat a where
    toInteger :: a -> Integer

data Zero
data Succ a

instance MyTypeNat Zero where
    toInteger _ = 0

instance MyTypeNat a => MyTypeNat (Succ a) where
    toInteger _ = toInteger (undefined :: a) + 1

data KDTree a b = -- ...

dimension :: forall a b. MyTypeNat a => KDTree a b -> Integer
dimension = toInteger (undefined :: a)

Недостатъкът на подход като този разбира се е, че трябва да напишете нещо като KDTree (Succ (Succ (Succ Zero))) Foo вместо KDTree 3 Foo.

person sepp2k    schedule 01.09.2011
comment
Разбира се, но тогава тип Three = Succ (Succ (Succ Zero)) ще помогне. - person Ingo; 01.09.2011
comment
Ако ще използвате само малки числа, можете също така да ги кодирате директно: данни едно / данни две / данни три / данни четири - по-лесно е за четене. - person firefrorefiddle; 02.09.2011

arrow_upward
3
arrow_downward

Отговорът на sepp2k показва основния подход за извършване на това. Всъщност голяма част от работата вече е свършена.

Пакети с номера на ниво тип

Неща, използващи кодиране на естествени числа на ниво тип (примери)

За съжаление нещо подобно:

data KDTree Int a = ...

не е наистина възможно. Крайният тип (конструиран от KDTree) зависи от стойността на Int, което изисква функция, наречена зависими типове. Езици като Agda и Epigram поддържат това, но не и Haskell.

person John L    schedule 01.09.2011
comment
Благодаря за това. Vec изглежда като най-простият възможен пример за мен, за да науча как да направя това. - person Joseph Victor; 01.09.2011
comment
Да, Vec е може би най-простият, след това Dimensional. llvm и ForSyDe са по-сложни, въпреки че мисля, че и двамата просто прилагат същото нещо като Vec. - person John L; 02.09.2011