Как работать с типами, которые меняются под композицией? - PullRequest
Новая
       43

Как работать с типами, которые меняются под композицией?

8 голосов
/ 06 мая 2019

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

Я думал, что, вероятно, можно будет смоделировать это в Haskell, поскольку описанные в статье sfun кажутся «просто еще одним экземпляром Arrow», поэтому я решил создать очень маленький POC.

Однако я столкнулся с проблемой, заключающейся в том, что существует четыре вида «тоничности» (из-за отсутствия лучшего термина): монотонный, антитонический, постоянный (который является одновременно) и неизвестный (который не является ни одним), которые могут превращаться друг в друга по составу или применению:

Когда применяются две «тонические функции», тоничность результирующей тонической функции должна быть самой специфической, которая соответствует обоим типам («Сокращение квалификатора; рис. 7» в статье):

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

Когда составлены две «тонические функции», тоничность результирующей тонической функции может измениться («Состав квалификатора; Рисунок 6» в документе):

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

У меня есть проблема с тем, чтобы правильно выразить это (связь между тонусами и тем, как составляются «тонические функции») в типах Haskell. Моя последняя попытка выглядит следующим образом с использованием GADT, семейства типов, DataKinds и множества других программных конструкций на уровне типов: 

{-# LANGUAGE GADTs, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, UndecidableInstances, KindSignatures, DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
module Main2 where

import qualified Control.Category
import Control.Category (Category, (>>>), (<<<))

import qualified Control.Arrow
import Control.Arrow (Arrow, (***), first)


main :: IO ()
main =
  putStrLn "Hi!"

data Tonic t a b where
  Tonic :: Tonicity t => (a -> b) -> Tonic t a b
  Tonic2 :: (TCR t1 t2) ~ t3 => Tonic t1 a b -> Tonic t2 b c -> Tonic t3 a c

data Monotonic = Monotonic
data Antitonic = Antitonic
class Tonicity t

instance Tonicity Monotonic
instance Tonicity Antitonic

type family TCR (t1 :: k) (t2 :: k) :: k where
  TCR Monotonic Antitonic = Antitonic
  TCR Antitonic Monotonic = Antitonic
  TCR t t = Monotonic


--- But now how to define instances for Control.Category and Control.Arrow?

У меня такое чувство, что я сильно усложняю вещи. Еще одна попытка, которую я ввел 

class (Tonicity a, Tonicity b) => TonicCompose a b where
  type TonicComposeResult a b :: *

, но невозможно использовать TonicComposeResult в объявлении экземпляра, например, Control.Category («Приложение экземпляра недопустимого семейства синонимов»).

Чего мне не хватает? Как правильно выразить эту концепцию в коде безопасного типа?

1 Ответ

5 голосов
/ 06 мая 2019

Множество тональностей фиксировано, поэтому один тип данных будет более точным. Конструкторы данных поднимаются до уровня типа с расширением DataKinds. 

data Tonicity = Monotone | Antitone | Constant | Unknown

Тогда я бы использовал новый тип для представления тонических функций: 

newtype Sfun (t :: Tonicity) a b = UnsafeMkSfun { applySfun :: a -> b }

Для обеспечения безопасности конструктор должен быть скрыт по умолчанию. Но пользователи такого Haskell EDSL, скорее всего, захотят включить в него свои собственные функции. Пометить имя конструктора как «unsafe» - хороший компромисс, чтобы включить этот вариант использования.

Композиция функций буквально ведет себя как композиция функций с некоторой дополнительной информацией на уровне типов. 

composeSfun :: Sfun t1 b c -> Sfun t2 a b -> Sfun (ComposeTonicity t1 t2) a c
composeSfun (UnsafeMkSfun f) (UnsafeMkSfun g) = UnsafeMkSfun (f . g)

-- Composition of tonicity annotations
type family ComposeTonicity (t1 :: Tonicity) (t2 :: Tonicity) :: Tonicity where
  ComposeTonicity Monotone Monotone = Monotone
  ComposeTonicity Monotone Antitone = Antitone
  ...
  ComposeTonicity _ _ = Unknown  -- Any case we forget is Unknown by default.
                                 -- In a way, that's some extra safety.
...