Какие функциональные зависимости требуется для этого безопасного по размеру варианта ZipWith и почему? - PullRequest
Новая
       25

Какие функциональные зависимости требуется для этого безопасного по размеру варианта ZipWith и почему?

1 голос
/ 16 февраля 2012

Я пытаюсь определить операции со списками, длина которых зависит от типа. В итоге у меня довольно много ограничений на эти списки (Map, Fold, что у вас), поэтому я бы хотел использовать новый GHC ConstraintKinds, чтобы немного упростить свою жизнь. Тем не менее, я не могу понять их.

Рассмотрим следующий (существенно упрощенный) пример: 

-- A list where length is implicit in the type.
-- This allows us to have classes like
-- Combineable a b c  u v w | ... where
--    combine :: (a -> b -> c) -> u -> v -> w
-- which is a version of ZipWith that only works on
-- lists of the same length.
data a :. b = !a :. !b

-- A simple class that works on our length-implicit lists
class Fold v a | v -> a where
  fold  :: (a -> a -> a) -> v -> a
instance Fold (a:.()) a where
  fold  f   (a:._) = a
instance Fold (a':.u) a => Fold (a:.a':.u) a where
  fold  f   (a:.v) = f a (fold f v)

-- A type constraint to simplify the constraints on our functions,
-- which in the real world also contain a bunch of things like
-- Map a a v v, Combineable a (Maybe a) (Maybe a) v w w, etc.
type NList v i = ( Fold (v i) i )

-- A function that uses our type constraint
foo :: (Num a, NList v a) -> v a -> a
foo = fold (+) 1

Выглядит довольно вменяемым для меня. Правильно? Неправильно. 

> foo ((1::Int) :. ())

Couldn't match type `Int' with `()'
When using functional dependencies to combine
  Fold (a :. ()) a,
    arising from the dependency `v -> a'
    in the instance declaration in `Data.Vec.Base'
  Fold (Int :. ()) (),
    arising from a use of `foo' at <interactive>:72:1-4
In the expression: foo ((1 :: Int) :. ())
In an equation for `it': it = foo ((1 :: Int) :. ())

Для меня это сообщение об ошибке примерно переводится как «почему вы пытаетесь программировать на уровне типа?»

Очевидно, я не совсем понимаю значение Constraint Kinds, но я не уверен, где я ошибся здесь. Кто-нибудь может обнаружить ошибку?

1 Ответ

2 голосов
/ 16 февраля 2012

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

Тип v в 

type NList v i = ( Fold (v i) i )

Кажется, конфликтует с видом v в Fold

class Fold v a | v -> a where
    fold  :: (a -> a -> a) -> v -> a

Код работает для меня, если мы просто удалим определение NList и изменим foo to 

foo :: (Num a, Fold v a) => v -> a
foo = fold (+)

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

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FunctionalDependencies #-}

data a :. b = !a :. !b
infixr 5 :.

Теперь мы можем запустить foo вGHCi 

*Main> foo (1:.())
1
*Main> foo (1:.2:.3:.())
6
...