Типы продуктов Currying

Используя семейства типов, мы можем определить функцию fold над типом и лежащую в основе алгебру для этого типа, представленную как n-набор функций и постоянных значений. Это позволяет определить обобщенную функцию foldr, определенную в классе Foldable type:

import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as S
import qualified Data.Map as M

class Foldable m where
  type Algebra m b :: *
  fold :: Algebra m b -> m -> b

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = (b, a -> b -> b)
  fold = uncurry $ flip S.fold

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = (b, k -> a -> b -> b)
  fold = uncurry $ flip M.foldWithKey

Аналогично, виды ограничений допускают определение обобщенной функции отображения. Функция карты отличается от fmap рассмотрением каждого поля значений типа алгебраических данных:

class Mappable m where
  type Contains m     :: *
  type Mapped   m r b :: Constraint
  map :: (Mapped m r b) => (Contains m -> b) -> m -> r

instance (Ord a) => Mappable (Set a) where
  type Contains (Set a)     = a
  type Mapped   (Set a) r b = (Ord b, r ~ Set b)
  map = S.map

instance (Ord k) => Mappable (Map k a) where
  type Contains (Map k a)     = (k, a)
  type Mapped   (Map k a) r b = (Ord k, r ~ Map k b)
  map = M.mapWithKey . curry

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

Curry :: Product -> Type -> Type
Curry ()       m = m
Curry (a × as) m = a -> (Curry as m b)

Если это так, мы могли бы сгенерировать фреймовую функцию из основной алгебры. Например:

  fold :: Curry (Algebra [a] b) ([a] -> b)
≡ fold :: Curry (b, a -> b -> b) ([a] -> b)
≡ fold :: b -> (Curry (a -> b -> b)) ([a] -> b)
≡ fold :: b -> (a -> b -> b -> (Curry () ([a] -> b))
≡ fold :: b -> ((a -> b -> b) -> ([a] -> b))

  map :: (Mapped (Map k a) r b) => (Curry (Contains (Map k a)) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (Curry (k, a) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (Curry (a) b) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (a -> Curry () b)) -> Map k a -> r
≡ map :: (Mapped (Map k a) r b) => (k -> (a -> b)) -> Map k a -> r

Я знаю, что Haskell не имеет функций типа, и правильное представление n-кортежа, вероятно, будет чем-то вроде типа типов с индексом типа. Возможно ли это?

EDIT: Для полноты моей текущей попытки решения прилагается ниже. Я использую пустые типы данных для представления продуктов типов и типа семейств, чтобы представить функцию Curry выше. Это решение, похоже, работает для функции отображения, но не для функции сгиба. Я верю, но не уверен, что Curry не восстанавливается должным образом при проверке типов.

data Unit
data Times a b

type family Curry a m :: *
type instance Curry Unit        m = m
type instance Curry (Times a l) m = a -> Curry l m

class Foldable m where
  type Algebra m b :: *
  fold :: Curry (Algebra m b) (m -> b)

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = Times (a -> b -> b) (Times b Unit)
  fold = S.fold

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = Times (k -> a -> b -> b) (Times b Unit)
  fold = M.foldWithKey

 class Mappable m where
   type Contains m     :: *
   type Mapped   m r b :: Constraint
   map :: (Mapped m r b) => Curry (Contains m) b -> m -> r

 instance (Ord a) => Mappable (Set a) where
   type Contains (Set a)     = Times a Unit
   type Mapped   (Set a) r b = (Ord b, r ~ Set b)
   map = S.map

 instance (Ord k) => Mappable (Map k a) where
   type Contains (Map k a)     = Times k (Times a Unit)
   type Mapped   (Map k a) r b = (Ord k, r ~ Map k b)
   map = M.mapWithKey

Ответ 1

Хорошо, я думаю, что мой другой ответ на самом деле не является ответом на ваш вопрос. Извините за это.

В своем последнем коде сравните типы fold и map:

fold :: Curry (Algebra m b) (m -> b)
map  :: (Mapped m r b) => Curry (Contains m) b -> m -> r

Здесь существенная разница. Тип fold - это просто семейное приложение типа, тогда как тип map содержит окончательный m -> r, указав параметр класса m. Таким образом, в случае map для GHC легко узнать, на каком типе вы хотите, чтобы экземпляр класса из контекста.

Не так в случае fold, к сожалению, потому что семейства типов не должны быть инъективными, и поэтому их нелегко инвертировать. Поэтому, видя конкретный тип, который вы используете fold at, для GHC невозможно сделать вывод, что m.

Стандартное решение этой проблемы - использовать аргумент прокси, который фиксирует тип m, определяя

data Proxy m = P

а затем вместо fold введите этот тип:

fold :: Proxy m -> Curry (Algebra m b) (m -> b)

Вам нужно адаптировать экземпляры для принятия и отбросить аргумент прокси. Затем вы можете использовать:

fold (P :: Proxy (Set Int)) (+) 0 (S.fromList [1..10])

или аналогично вызову функции fold на наборах.

Чтобы более четко понять, почему эта ситуация сложна для решения GHC, подумайте об этом примере с игрушкой:

class C a where
  type F a :: *
  f :: F a

instance C Bool where
  type F Bool = Char -> Char
  f = id

instance C () where
  type F () = Char -> Char
  f = toUpper

Теперь, если вы вызываете f 'x', для GHC нет значимого способа определить, какой экземпляр вы имели в виду. Прокси также поможет здесь.

Ответ 2

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

Ниже приводится объяснение, как достичь этого как отдельного шага. Да, это также можно сделать все сразу, я уже делал что-то подобное раньше. Однако, я думаю, что отдельная фаза дает понять, что происходит.

Нам нужны следующие расширения языка:

{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances #-}

Я использую следующие типы продуктов и единиц:

data U = U
data a :*: b = a :*: b

infixr 8 :*:

В качестве примера предположим, что у нас есть неудобная версия складки на списках:

type ListAlgType a r = (U -> r)
                   :*: (a :*: r :*: U -> r)
                   :*: U

inconvenientFold :: ListAlgType a r -> [a] -> r
inconvenientFold   (nil :*: cons :*: U) []       = nil U
inconvenientFold [email protected](nil :*: cons :*: U) (x : xs) = cons (x :*: inconvenientFold a xs :*: U)

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

class CurryInner a where
  type CurryI a k :: *
  curryI   :: (a -> b) -> CurryI a b
  uncurryI :: CurryI a b -> a -> b

class CurryOuter a where
  type CurryO a k :: *
  curryO   :: (a -> b) -> CurryO a b
  uncurryO :: CurryO a b -> (a -> b) -- not really required here

Каждый тип класса реализует изоморфизм между карьерами и неокрашенными типами. Типы типов выглядят одинаково, но CurryOuter будет вызывать CurryInner для каждого компонента внешнего вложенного кортежа.

Экземпляры относительно просты:

instance CurryInner U where
  type CurryI U k = k
  curryI f   = f U
  uncurryI x = \ U -> x

instance CurryInner ts => CurryInner (t :*: ts) where
  type CurryI (t :*: ts) k = t -> CurryI ts k
  curryI f   = \ t -> curryI (\ ts -> f (t :*: ts))
  uncurryI f = \ (t :*: ts) -> uncurryI (f t) ts

instance CurryOuter U where
  type CurryO U k = k
  curryO f   = f U
  uncurryO x = \ U -> x

instance (CurryInner a, CurryOuter ts) => CurryOuter ((a -> b) :*: ts) where
  type CurryO ((a -> b) :*: ts) k = CurryI a b -> CurryO ts k
  curryO f   = \ t -> curryO (\ ts -> f (uncurryI t :*: ts))
  uncurryO f = \ (t :*: ts) -> uncurryO (f (curryI t)) ts

Что это. Обратите внимание, что

*Main> :kind! CurryO (ListAlgType A R) ([A] -> R)
CurryO (ListAlgType A R) ([A] -> R) :: *
= R -> (A -> R -> R) -> [A] -> R

(для подходящих типов заполнителей A и R). Мы можем использовать его следующим образом:

*Main> curryO inconvenientFold 0 (+) [1..10]
55

Изменить: Теперь я вижу, что вы на самом деле спрашиваете только о том, как выкрасить внешний слой. Тогда вам нужен только один класс, но он может использовать ту же идею. Я использовал этот пример, потому что я написал что-то для общей библиотеки программирования, основанной на суммарном продукте, которая раньше требовала двух уровней каррирования, и сначала подумала, что вы находитесь в одной и той же настройке.

Ответ 3

Список типов уровня - это именно то, что вам нужно! Вы очень близки, но для этого вам нужна полная мощность как DataKinds, так и ScopedTypeVariables:

{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances, TypeFamilies, TypeOperators, ScopedTypeVariables #-}
import GHC.Exts (Constraint)
import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as S
import qualified Data.Map as M

-- | A "multifunction" from a list of inhabitable types to an inhabitable type (curried from the start).  
type family (->>) (l :: [*]) (y :: *) :: *
type instance '[] ->> y = y
type instance (x ': xs) ->> y = x -> (xs ->> y)

class Foldable (m :: *) where
  type Algebra m (b :: *) :: [*]
  fold :: forall (b :: *). Algebra m b ->> (m -> b)

instance (Ord a) => Foldable (Set a) where
  type Algebra (Set a) b = '[(a -> b -> b), b]
  fold = S.fold :: forall (b :: *). (a -> b -> b) -> b -> Set a -> b

instance (Ord k) => Foldable (Map k a) where
  type Algebra (Map k a) b = '[(k -> a -> b -> b), b]
  fold = M.foldWithKey :: forall (b :: *). (k -> a -> b -> b) -> b -> Map k a -> b

class Mappable m where
  type Contains m :: [*]
  type Mapped m (b :: *) (r :: *) :: Constraint
  map :: forall (b :: *) (r :: *). Mapped m b r => (Contains m ->> b) -> m -> r

instance (Ord a) => Mappable (Set a) where
  type Contains (Set a) = '[a]
  type Mapped (Set a) b r = (Ord b, r ~ Set b)
  map = S.map :: forall (b :: *). (Ord b) => (a -> b) -> Set a -> Set b

instance (Ord k) => Mappable (Map k a) where
  type Contains (Map k a) = '[k, a]
  type Mapped (Map k a) b r = r ~ Map k b
  map = M.mapWithKey :: forall (b :: *). (k -> a -> b) -> Map k a -> Map k b