如何处理根据组成而变化的类型？

Question

我最近读了一篇非常有趣的论文《单调类型》，其中描述了一种新的HM语言，该语言跟踪操作之间的单调性，因此程序员不必手动执行此操作（并且在非单调操作时会在编译时失败）传递给需要一个的东西）。

我当时认为可能可以在Haskell中对此建模，因为sfun本文描述的s似乎只是“另一个Arrow实例”，所以我着手创建一个非常小的POC。

但是，我碰到一个问题，简单地说，存在四种“音调”（由于缺乏更好的用语）：单调，反调，常数（两者都是）和未知（两者都不是），它们可以转变为在组成或应用中彼此融合：

当应用两个“补声函数”时，所得的补声函数的语调应该是与两种类型都匹配的最具体的补语（本文中的“限定词收缩；图7”）：

• 如果两者都是恒定的张力，则结果应该是恒定的。
• 如果两者都是单调的，则结果应该是单调的
• 如果两者都是反渗透的，则结果应该是反渗透的
• 如果一个是常数而另一个是单调的，则结果应该是单调的
• 如果一个是常数而另一个是反渗透的，则结果应该是反渗透的
• 如果一个是单调的而一个是反调的，则结果应该是未知的。
• 如果其中一个未知，则结果未知。

当组成两个“音调函数”时，所得的音调函数的音调可能会翻转（本文中的“限定词组成；图6”）：

• 如果两者都是恒定的张力，则结果应该是恒定的。
• 如果两者都是单调的，则结果应该是单调的
• 如果两者都是反调的，则结果应该是单调的
• 如果一个是单调的而一个是反渗透的，则结果应该是反渗透的。
• 如果其中一个未知，则结果未知。

我有一个问题要用Haskell的类型恰当地表达这一点（语调之间的关系，以及“语调功能”的组成方式）。我最近的尝试是使用GADT，Type Families，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.