Как определить поливариадную стрелку? - PullRequest
Новая
       59

Как определить поливариадную стрелку?

2 голосов
/ 11 мая 2019

Этот вопрос в некоторой степени связан с ранее :

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

В более общем плане: я бы хотел отслеживать некоторые «квалификаторы» функции

Основываясь на ответах на этот предыдущий вопрос , я смог определить «индексированную категорию» и «индексированную стрелку», где квалификаторы h в h = f >>> g зависят от квалификаторов f и g.

Это работает хорошо, если вы работаете только с функциями с одним аргументом. Однако (и обычные стрелки также имеют эту проблему), когда вы пытаетесь создать стрелку с несколькими аргументами, у вас есть следующие опции. (Используя (+) :: Int -> Int -> Int в качестве примера):

  1. Обычный arr (+). Тип результата этого будет Arrow x => x Int (Int -> Int), так как функция карри. Это означает, что только первый параметр поднимается в контекст стрелки, поскольку стрелка «возвращает функцию с одним параметром меньше». Другими словами: контекст стрелки не используется для остальных аргументов, так что это не то, что мы хотим.
  2. arr (uncurry (+)). Тип результата этого будет Arrow x => x (Int, Int) Int. Теперь оба параметра стали частью стрелки, но мы теряем способность, например, частично примените это. Мне также непонятно, как делать неосуществление независимым от арности способом: что если нам нужны функции с тремя, четырьмя, пятью, ...- параметрами?

Я знаю, что можно определить «рекурсивный класс типов» для создания поливариадной функции, как, например, описано в Rosettacode здесь . Я попытался определить более общий тип переноса функций, который мог бы работать таким образом, но мне пока не удалось сделать это. Я понятия не имею, как правильно определить в экземпляре класса типов для a -> b, является ли b конечным результатом или другой функцией (b' -> c), и как извлечь и использовать квалификатор b', если он окажется второй случай.

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

1 Ответ

3 голосов
/ 11 мая 2019

Вот как вы можете определить arrowfy, чтобы превратить функцию a -> b -> ... в стрелку a `r` b `r` ... (где r :: Type -> Type -> Type - ваш тип стрелки), и функцию uncurry_, чтобы превратить функцию в единицу с однимАргумент кортежа (a, (b, ...)) -> z (который затем можно поднять на произвольную стрелку с помощью arr :: (u -> v) -> r u v). 

{-# LANGUAGE
    AllowAmbiguousTypes,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    UndecidableInstances,
    TypeApplications
  #-}

import Control.Category hiding ((.), id)
import Control.Arrow
import Data.Kind (Type)

В обоих подходах используется класс многопараметрических типов с перекрывающимися экземплярами.Один экземпляр для функций, который будет выбран, пока начальный тип является типом функции, и один экземпляр для базового случая, который будет выбран, как только это не тип функции. 

-- Turn (a -> (b -> (c -> ...))) into (a `r` (b `r` (c `r` ...)))
class Arrowfy (r :: Type -> Type -> Type) x y where
  arrowfy :: x -> y

instance {-# OVERLAPPING #-} (Arrow r, Arrowfy r b z, y ~ r a z) => Arrowfy r (a -> b) y where
  arrowfy f = arr (arrowfy @r @b @z . f)

instance (x ~ y) => Arrowfy r x y where
  arrowfy = id

Примечание о синтаксисе arrowfy @r @b @z

Это синтаксис TypeApplications, доступный с GHC 8.0.

Тип arrowfy: 

arrowfy :: forall r x y. Arrowfy r x y => x -> y

Проблема в том, что rнеоднозначный: в выражении контекст может определять только x и y, и это не обязательно ограничивает r.Аннотация @r позволяет нам явно специализировать arrowfy.Обратите внимание, что аргументы типа arrowfy должны появляться в фиксированном порядке: 

arrowfy :: forall r x y. ...

arrowfy @r1 @b @z             -- r = r1, x = b, y = z

( Руководство пользователя GHC на TypeApplications)

Теперь дляНапример, если у вас есть стрелка (:->), вы можете написать это, чтобы превратить ее в стрелку: 

test :: Int :-> (Int :-> Int)
test = arrowfy (+)

Для uncurry_ есть небольшой дополнительный трюк, так что функции с n аргументами превращаютсяв функции из n-кортежей, а не (n + 1) -пакетов, ограниченных единицей, которую вы наивно получите.Оба экземпляра теперь индексируются по типам функций, и на самом деле проверяется, является ли тип результата функцией. 

-- Turn (a -> (b -> (c -> ... (... -> z) ...))) into ((a, (b, (c, ...))) -> z)
class Uncurry x y z where
  uncurry_ :: x -> y -> z

instance {-# OVERLAPPING #-} (Uncurry (b -> c) yb z, y ~ (a, yb)) => Uncurry (a -> b -> c) y z where
  uncurry_ f (a, yb) = uncurry_ (f a) yb

instance (a ~ y, b ~ z) => Uncurry (a -> b) y z where
  uncurry_ = id

Некоторые примеры: 

testUncurry :: (Int, Int) -> Int
testUncurry = uncurry_ (+)

-- combined with arr
testUncurry2 :: (Int, (Int, (Int, Int))) :-> Int
testUncurry2 = arr (uncurry_ (\a b c d -> a + b + c + d))

Полный текст: https://gist.github.com/Lysxia/c754f2fd6a514d66559b92469e373352

...