如何处理在组合下发生变化的类型？

Question

我最近读了一篇非常有趣的论文单调性类型，其中描述了一种新的 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

（“实例中非法类型同义词族应用”）。

---

我错过了什么？如何在类型安全代码中正确表达这个概念？

Answer 1

张力范围是固定的，因此单一数据类型会更准确。数据构造函数通过

DataKinds

扩展提升到类型级别。

data Tonicity = Monotone | Antitone | Constant | Unknown

然后，我会使用一个新类型来表示补品功能：

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

为了保证安全，构造函数必须默认隐藏。但此类 Haskell EDSL 的用户很可能希望将自己的函数封装在其中。用“不安全”标记构造函数的名称是启用该用例的一个很好的折衷方案。

函数组合实际上表现为函数组合，带有一些额外的类型级信息。

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.