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

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

7 голосов
/ 01 сентября 2011

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

Я пытался параметризовать свое дерево с помощью кортежей, но оно, похоже, никуда не денется (и кажется маловероятным, что это можно будет протолкнуть, тем более что не похоже, что это утроится или что-то еще).больше даже функторы (и я не знаю, как сказать, например, экземпляр HomogeneTuple 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 -> * -> *

Кто-нибудь знает, является ли какой-либо из этих эффектов осуществимым или разумным?

Спасибо -Joseph

Ответы [ 2 ]

5 голосов
/ 01 сентября 2011

Работает расширение 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.

3 голосов
/ 01 сентября 2011

Ответ sepp2k показывает основной подход к этому. На самом деле, большая часть работы уже выполнена.

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

Материал с использованием кодировок натуральных чисел на уровне типов (примеры)

К сожалению что-то вроде этого: 

data KDTree Int a = ...

не реально возможно. Окончательный тип (созданный KDTree) зависит от значения Int, для которого требуется функция, называемая зависимыми типами. Такие языки, как Agda и Epigram, поддерживают это, но не Haskell.

...