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

Я пытаюсь создать некоторые типы Haskell, которые параметризованы не типами, а элементами типа, в частности, целыми числами. Например, вектор (линейной алгебры) в R^2 и вектор в R^3 являются объектами разных типов. В частности, я пишу KD-дерево в Haskell и хочу параметризовать свою структуру данных положительным целым числом, чтобы трехмерное дерево и четырехмерное дерево имели разные типы.

Я пытался параметризовать свое дерево с помощью кортежей, но это, похоже, никуда не денется (и кажется несколько маловероятным, что это можно протолкнуть, тем более, что тройки или что-то большее не похоже даже на функторы (и Я не знаю, как сказать, например, экземпляр 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
Да, Век наверное самый простой, потом Пространственный. llvm и ForSyDe более сложны, хотя я думаю, что они оба просто реализуют то же самое, что и Vec. - person John L; 02.09.2011