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

Question

我最近阅读了一篇非常有趣的论文 Monotonicity Types其中描述了一种新的 HM 语言，它跟踪操作的单调性，因此程序员不必手动执行此操作(并且当非单调操作传递给需要的东西时，编译时会失败)。

我在想可能有可能在 Haskell 中对此进行建模，因为 sfun论文描述的 s 似乎“只是另一个 Arrow 实例”，因此我着手创建一个非常小的 POC。

但是，我遇到了一个问题，简单地说，有四种“张力”(因为没有更好的术语):单调的、反调的、恒定的(两者都是)和未知的(两者都不是)，它们可以转动在组合或应用下相互成对:

当应用两个“补品函数”时，生成的补品函数的补品应该是与这两种类型匹配的最具体的补品(论文中的“限定符收缩；图 7”):

如果两者都是恒定的张力，则结果应该是恒定的。

如果两者都是单调的，则结果应该是单调的

如果两者都是antitonic，结果应该是antitonic

如果一个是常数而另一个是单调的，则结果应该是单调的

如果一个是恒定的，另一个是反调的，结果应该是反调的

如果一个是单调的，一个是反调的，结果应该是未知的。

如果其中任何一个未知，则结果未知。

当组合两个“补品函数”时，生成的补品函数的补品可能会翻转(“限定符组合；论文中的图 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.