Рекурсивно определенные экземпляры и ограничения

Я играю с векторами и матрицами, где размер кодируется в их типе, используя новое расширение DataKinds. В основном это происходит следующим образом:

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

Теперь нам нужны типичные экземпляры типа Functor и Applicative. Functor легко:

instance Functor (Vector n) where
    fmap f VNil = VNil
    fmap f (VCons a v) = VCons (f a) (fmap f v)

Но с экземпляром Applicative возникает проблема: мы не знаем, какой тип должен возвращаться в чистом виде. Однако мы можем определить экземпляр индуктивно по размеру вектора:

instance Applicative (Vector Zero) where
    pure = const VNil
    VNil <*> VNil = VNil

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where
    pure a = VCons a (pure a)
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v)

Однако, хотя этот экземпляр применяется ко всем векторам, средство проверки типов не знает этого, поэтому мы должны нести ограничение Applicative каждый раз, когда мы используем экземпляр.

Теперь, если это применимо только к экземпляру Applicative, это не будет проблемой, но оказывается, что трюк рекурсивных деклараций экземпляров необходим при программировании с такими типами. Например, если мы определяем матрицу как вектор векторов строк с использованием библиотеки TypeCompose,

type Matrix nx ny a = (Vector nx :. Vector ny) a

мы должны определить класс типа и добавить рекурсивные объявления экземпляра для реализации как транспонирования, так и матричного умножения. Это приводит к огромному распространению ограничений, которые нам приходится выполнять каждый раз, когда мы используем код, даже если экземпляры действительно применяются ко всем векторам и матрицам (что делает ограничения бесполезными).

Есть ли способ избежать необходимости переносить все эти ограничения? Можно ли расширить проверку типа, чтобы он мог обнаружить такие индуктивные конструкции?

Ответы

Ответ 1

Определение pure действительно лежит в основе проблемы. Каким должен быть его тип, полностью количественный и квалифицированный?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x            -- (X)

не будет выполняться, так как во время выполнения нет информации, чтобы определить, должен ли pure испускать VNil или VCons. Соответственно, как обстоят дела, вы не можете просто

instance Applicative (Vector n)                                -- (X)

Что вы можете сделать? Хорошо, работая с Strathclyde Haskell Enhancement, в файле Vec.lhs, я определяю предшественник pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x
vec {Zero}    x = VNil
vec {Succ n}  x = VCons x (vec n x)

с типом pi, требующим, чтобы во время выполнения была передана копия n. Это pi (n :: Nat). desugars как

forall n. Natty n ->

где Natty, с более прозаическим именем в реальной жизни, является singleton GADT, данный

data Natty n where
  Zeroy :: Natty Zero
  Succy :: Natty n -> Natty (Succ n)

и фигурные скобки в уравнениях для vec просто перевести конструкторы Nat в конструкторы Natty. Затем я определяю следующий дьявольский экземпляр (отключение экземпляра Functor по умолчанию)

instance {:n :: Nat:} => Applicative (Vec {n}) where
  hiding instance Functor
  pure = vec {:n :: Nat:} where
  (<*>) = vapp where
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t
    vapp  VNil          VNil          = VNil
    vapp  (VCons f fs)  (VCons s ss)  = VCons (f s) vapp fs ss

который требует дальнейших технологий. Ограничение {:n :: Nat:} desugars на то, что требует наличия свидетеля Natty n, и по силе переменных типа с областью действия - те же {:n :: Nat:} повестки, которые явно указаны. Longhand, это

class HasNatty n where
  natty :: Natty n
instance HasNatty Zero where
  natty = Zeroy
instance HasNatty n => HasNatty (Succ n) where
  natty = Succy natty

и заменим ограничение {:n :: Nat:} на HasNatty n и соответствующий член с (natty :: Natty n). Выполнение этой конструкции систематически сводится к написанию фрагмента типа Haskell typechecker в классе класса Prolog, который не является моей идеей радости, поэтому я использую компьютер.

Обратите внимание, что экземпляр Traversable (извините мои скобки идиомы и мои бесшумные экземпляры Functor и Foldable по умолчанию) не требует такого pigery jiggery

instance Traversable (Vector n) where
  traverse f VNil         = (|VNil|)
  traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|)

Чтобы вся структура вам нужна, чтобы получить матричное умножение без дальнейшей явной рекурсии.

TL; DR Используйте конструкцию singleton и связанный с ней тип класса, чтобы свернуть все рекурсивно определенные экземпляры с наличием свидетеля времени выполнения для данных типа уровня, из которых вы можете вычислить путем явной рекурсии.

Каковы последствия дизайна?

GHC 7.4 обладает технологией продвижения по типу, но у SHE все еще есть конструкции типа pi. Одно из важных моментов в продвинутых типах данных заключается в том, что они закрыты, но на самом деле они пока еще не проявляются чисто: конструктивность одиночных свидетелей является проявлением этой замкнутости. Как бы то ни было, если у вас есть forall (n :: Nat)., тогда всегда разумно требовать и одноэлементный, но для этого имеет значение сгенерированный код: явный ли он как в моей конструкции pi или неявный, как в словаре для {:n :: Nat:}, имеется дополнительная информация о времени выполнения, и, соответственно, более слабая свободная теорема.

Открытый вопрос проектирования для будущих версий GHC заключается в том, как управлять этим различием между присутствием и отсутствием свидетелей времени выполнения для данных типа. С одной стороны, мы нуждаемся в них в ограничениях. С другой стороны, нам нужно сопоставить шаблон с ними. Например, если pi (n :: Nat). означает явное

forall (n :: Nat). Natty n ->

или неявный

forall (n :: Nat). {:n :: Nat:} =>

? Конечно, языки, подобные Agda и Coq, имеют две формы, поэтому, возможно, Haskell должен последовать этому примеру. Конечно, есть место для прогресса, и мы над этим работаем!