时间戳

首页 > 解决方案 > 如何处理在组合下发生变化的类型？

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

问题描述

我最近阅读了一篇非常有趣的论文Monotonicity Types，其中描述了一种新的 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在 eg 的实例声明中使用Control.Category（"illegal type synonym family application in instance"）。

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

标签： haskellarrowstype-level-computation

解决方案

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

推荐阅读