0

以下断言是否正确：

  1. 唯一真正的同构，用户可以通过编程方式访问，由 Haskell 类型系统验证，并且 Haskell 编译器是/可以知道的，是：

    • Haskell 数据类型的一组值
    • 其构造函数所需的类型值的集合

  2. 即使是通用编程也不能产生“真正的”同构，其组合在运行时会产生一个身份（因此staged-sop -在Ocaml中也是如此）

  3. Haskell 本身是唯一产生同构的Coercible，但那些同构仅限于恒等同构

“真正的同构，用户可以通过编程方式访问，由 Haskell 类型系统验证，并且 Haskell 编译器是/可以知道的”我的意思是一对函数u : a -> b，并且v : b -> aHaskell知道（通过被告知或以其他方式）u.v=id并且v.u=id. 就像它知道（在编译时）如何重写一些代码来进行“折叠融合”，这类似于立即识别并应用它。

4

1 回答 1

4

查看同伦类型理论/立方Agda，其中“平等是同构”。我对它不够熟悉，不知道操作上会发生什么，即使 Agda 知道同构类型是相等的，我仍然认为你的“真正的同构”（即具有证明和融合）太高了。

在 GHC 中，可以通过“同构”派生，但我们需要等待依赖类型才能正确验证类型系统中的同构。即便如此，即使您必须在操作上做一些工作，它们也可以用来生成真正的代码。

您已经提到了“代表性平等”（Coercible），但值得讨论。它支持coerce基于两个的推导策略：GeneralizedNewtypeDeriving并且DerivingVia概括了 GND。

GND 是将同构 ( Coercible USD Int) 转换为代码的最简单方法：

type    USD :: Type
newtype USD = MkUSD Int
  deriving
  newtype (Eq, Ord, Show, Num)

运营coerce成本为零，因此它们在运行时不会产生任何成本。这是你在 Haskell 中得到你想要的东西的唯一方法。

同构也可以通过用户定义的类型类来完成。

Representable f一个手段的实例f（自然地）与其表示对象的函数同构(Rep f ->)。newtype使用这种同构来派生可Co表示函子的函数实例。Pair a两个值的A由 表示Bool，因此与 同构Bool -> a。

这种同构可以Pair派生Functor，Applicative并Monad通过往返(Bool ->)：

type Pair :: Type -> Type
data Pair a = a :# a
  deriving (Functor, Applicative, Monad)
  via Co Pair

instance Distributive Pair where
  distribute :: Functor f => f (Pair a) -> Pair (f a)
  distribute = distributeRep

instance Representable Pair where
  type Rep Pair = Bool

  index :: Pair a -> (Bool -> a)
  index (false :# true) = \case
    False -> false
    True  -> true

  tabulate :: (Bool -> a) -> Pair a
  tabulate make = make False :# make True

当您派生Generic/时Generic1，编译器会在泛型类型与其泛型表示Rep/之间生成同构（不要与上面示例Rep1中的表示对象混淆）。Rep

阶级法规定to/from和to1/from1见证了同构。类型系统不强制执行这些法律，但如果您派生它们，它们应该遵守。

它们是在 Haskell 中定义泛型实现的主要方式。我最近介绍了两个新类型Generically和base，作为通用行为的标准名称（在下一个 GHC 版本之前使用generic-data ）。您可以派生通用同构并以编程方式在下一行中使用它，而无需离开声明：Generically1data

type Lists :: Type -> Type
data Lists a = Lists [a] [a] [a]
  deriving
  stock (Show, Generic, Generic1)

  deriving (Semigroup, Monoid)
  via Generically (Lists a)

  deriving (Functor, Applicative, Alternative)
  via Generically1 Lists

>> mempty @(Lists _)
Lists [] [] []
>> empty @Lists
Lists [] [] []
>> Lists "a" "b" "c" <> Lists "!" "." "?"
Lists "a!" "b." "c?"
>> pure @Lists 'a'
Lists "a" "a" "a"

但是，您将不得不支付转换成本，这并不像添加那么简单，{-# Rules "to/from" to . from = id #-}因为实际实例将出现中间项，例如to (from a <> from b). 即使您的“真正的同构”GHC 也无法融合转换，因为它不是to . from.

还有一个库iso-deriving（博客）允许通过任意同构派生。

于 2022-02-18T19:13:45.977 回答