Объявление экземпляров синонимов параметризованного типа

У меня есть куча функций, которые работают с Vectors, т.е. списками с длинами с типом.

Я пытаюсь сделать мои типы более легкими для записи, т.е. вместо записи

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ...

Я объявляю новый класс NList, поэтому могу просто написать foo :: NList v Integer => ...

Класс (упрощенный) выглядит следующим образом:

class ( Fold (v i) i
      , Map i i (v i) (v i)
      , Map i (Maybe i) (v i) (v (Maybe i))
      ) => NList v i

Как вы можете видеть, я должен хранить "векторный" тип отдельно от типа "item" (т.е. v отдельно от i), чтобы я мог делать такие вещи, как Map, на Maybe вектор.

Таким образом, v должен иметь вид * -> * и i kind *.

Однако, когда я пытаюсь создать экземпляр с такими векторами:

instance NList Vec2 Integer
instance NList Vec3 Integer
...

Я получаю следующую ошибку:

Type synonym `Vec2' should have 1 argument, but has been given none
In the instance declaration for `NList Vec2 Integer'

Теперь, я очень новичок в программировании на уровне шрифта, и я понимаю, что, скорее всего, я сделаю это очень обратным образом. Возможно ли создать экземпляр синонима типа? У любого типа-волшебники есть предложения по лучшим способам достижения моих целей?

Ответ 1

Проблема здесь в том, что Vec2 и Vec3 предположительно объявлены как что-то вроде этого:

type Vec2 a = Vec (S (S Z)) a
type Vec3 a = Vec (S (S (S Z))) a

Синонимы типов не могут быть частично применены по разным тайным причинам (они приведут к ямбам уровня типа, которые разрушают хаос со всеми вещами, связанными с разрешением и умозаключением экземпляра - представьте, если бы вы могли определить type Id a = a и сделать это экземпляр Monad).

То есть вы не можете сделать Vec2 экземпляр чего-либо, потому что вы не можете использовать Vec2, как если бы он был конструктором с полным fledge с типом * -> *; это фактически макрос уровня типа, который может быть применен только полностью.

Однако вы можете определить синонимы типов как частичные приложения:

type Vec2 = Vec (S (S Z))
type Vec3 = Vec (S (S (S Z)))

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

Если ваш тип Vec3 действительно выглядит как

type Vec3 a = Cons a (Cons a (Cons a Nil)))

или подобное, тогда вам не повезло; вам нужно будет использовать обертку newtype, если вы хотите предоставить какие-либо экземпляры. (С другой стороны, вы должны быть в состоянии избежать определения экземпляров непосредственно на этих типах полностью путем предоставления экземпляров для Nil и Cons вместо этого, что позволяет использовать Vec3 как экземпляр.)

Обратите внимание, что при использовании GHC 7.4 новых типов ограничений вы можете полностью исключить отдельный тип и просто определить синтаксис ограничения:

type NList v i =
    ( Fold (v i) i
    , Map i i (v i) (v i)
    , Map i (Maybe i) (v i) (v (Maybe i))
    )

Насколько ваш подход в целом идет, он должен в основном работать нормально; эта же общая идея используется пакетом Vec. Огромное количество классов и больших контекстов может сделать сообщения об ошибках очень запутанными и замедлить компиляцию, но такова природа хакерства на уровне типа. Однако, если у вас есть базовый тип Vec, определенный как обычный GADT:

data Vec n a where
    Nil :: Vec Z a
    Succ :: a -> Vec n a -> Vec (S n) a

то вам вообще не нужны никакие классы. Если он определен каким-либо другим способом, но по-прежнему параметризуется на естественном уровне типа, то вы можете заменить все классы на один:

data Proxy s = Proxy

class Nat n where
    natElim
        :: ((n ~ Z) => r)
        -> (forall m. (n ~ S m, Nat m) => Proxy m -> r)
        -> Proxy n
        -> r

Это должно позволить вам полностью исключить контексты, но делает определение операций над векторами немного сложнее.