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

Question

我最近读了一篇非常有趣的论文 Monotonicity Types，其中描述了一种新的 HM 语言，它可以跟踪跨操作的单调性，这样程序员就不必手动执行此操作（并且在编译时失败-将非单调操作传递给需要单调操作的时间）。

我在想可能可以在 Haskell 中对此进行建模，因为论文描述的 sfun 似乎是 'just another Arrow instance'，所以我开始着手创建一个非常小的 POC。

然而，我遇到的问题是，简单地说，有四种'tonicities'（因为没有更好的术语）：单调的，反调的，常数（两者都是）和未知的（哪个两者都不是），在组合或应用下可以变成另一个：

当应用两个 'tonic functions' 时，生成的 tonic 函数的 tonicity 应该是匹配两种类型的最具体的一个（论文中的'Qualifier Contraction; Figure 7'）：

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

当两个'tonic functions'组合时，生成的tonic函数的tonicity可能会翻转（论文中的'Qualifier Composition; Figure 6'）：

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

我无法在 Haskell 的类型中正确表达这一点（强音之间的关系，以及 'tonic functions' 将如何组成）。我最近的尝试是这样的，使用 GADT、类型族、DataKind 和大量其他类型级编程结构：

{-# 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 ("illegal type synonym family application in instance")。

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

Answer 1

tonicities 的范围是固定的，因此单一数据类型会更准确。使用 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.

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

How to work with types that change under composition?

haskell

arrows

type-level-computation