Зависимо типизированные приложения ZipVector

Я сделал себе стиль "ZipVector" Applicative на конечных Vector, который использует тип суммы для склеивания конечных векторов с Unit, которые моделируют "бесконечные" векторы.

data ZipVector a = Unit a | ZipVector (Vector a)
             deriving (Show, Eq)

instance Functor ZipVector where
  fmap f (Unit a)  = Unit (f a)
  fmap f (ZipVector va) = ZipVector (fmap f va)

instance Applicative ZipVector where
  pure = Unit
  Unit f   <*> p        = fmap f p
  pf       <*> Unit x   = fmap ($ x) pf
  ZipVector vf <*> ZipVector vx = ZipVector $ V.zipWith ($) vf vx

Этого, вероятно, будет достаточно для моих нужд, но я лениво хотел, чтобы "Fixed Dimensional" был смоделирован на аппликативных экземплярах, которые вы можете получить с зависимо типизированными "Vector".

data Point d a = Point (Vector a) deriving (Show, Eq)

instance Functor (Point d) where
  fmap f (Point va) = Point (fmap f va)

instance Applicative Point where
  pure = Vector.replicate reifiedDimension
  Point vf <*> Point vx = Point $ V.zipWith ($) vf vx

где параметр фантома d является уровнем типа Nat. Как я могу (если это возможно) написать reifiedDimension на Haskell? Более того, опять же, если возможно, учитывая (Point v1) :: Point d1 a и (Point v2) :: Point d2 a, как я могу получить length v1 == length v2, могу ли я получить d1 ~ d2?


types vector haskell dependent-type
person J. Abrahamson    schedule 23.04.2013    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Как я могу (если это возможно) написать reifiedDimension на Haskell?

Использование GHC.TypeLits и ScopedTypeVariables:

instance SingI d => Applicative (Point d) where
  pure = Point . Vector.replicate reifiedDimension
    where reifiedDimension = fromInteger $ fromSing (sing :: Sing d)
  ...

См. мой ответ здесь для полного примера.

Более того, опять же, если возможно, учитывая (Point v1) :: Point d1 a и (Point v2) :: Point d2 a, как я могу получить length v1 == length v2, могу ли я получить d1 ~ d2?

С Data.Vector нет. Вам понадобится векторный тип, который кодирует длину в типе. Лучшее, что вы можете сделать, это поддерживать это самостоятельно и инкапсулировать, не экспортируя конструктор Point.

person hammar    schedule 24.04.2013
comment
Вы хотите сказать, что у вас есть умный конструктор, такой как toP :: Vector a -> Point d a, который отражает d :: Sing (Vector.length v)? Я пытался заставить это работать, но это терпит неудачу, и я еще не могу точно понять, что говорят ошибки типа. - person J. Abrahamson; 24.04.2013
comment
Когда я пытаюсь переформулировать это с чем-то вроде pLen :: SingI d => Point d a -> Sing d; pLen _ = sing, GHC жалуется, что есть No instance for (SingI Nat d0) arising from a use of pLen. - person J. Abrahamson; 24.04.2013
comment
Кроме того, зачем включать Maybe, если вроде бы работает такая функция, как hpaste.org/86438? - person J. Abrahamson; 24.04.2013
comment
@tel: Какое выражение вы пытаетесь оценить? Добавление Maybe гарантирует, что длина в типе соответствует фактической длине. Не было бы смысла использовать интеллектуальный конструктор, если бы вы могли просто использовать любой старый вектор. - person hammar; 24.04.2013
comment
Я бы хотел fmap pLen . toP === Просто . V.длина - person J. Abrahamson; 24.04.2013
comment
Ой! Понимаю. Типы уже унифицированы и стерты к моменту создания вектора, поэтому типы «d» уже будут идентифицированы и без «Может быть» просто пройдут без проверки. - person J. Abrahamson; 24.04.2013
comment
@tel: Да, проблема в том, что вы не можете составить fmap pLen . toP, не зная статически, какая длина уровня типа должна быть в середине. fmap pLen (toP ... :: Maybe (Point 3 Int)) и т. д. будут работать. - person hammar; 24.04.2013