Зависимо въведени приложения „ZipVector“.

Направих си стил "ZipVector" Applicative на крайни Vectors, който използва тип сума за залепване на крайни вектори към Units, които моделират "безкрайни" вектори.

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