表达无限种

Question

在Haskell中表达无限类型时：

f x = x x -- This doesn't type check

可以使用 newtype 来完成：

newtype Inf = Inf { runInf :: Inf -> * }

f x = x (Inf x)

是否存在允许表达无限种类的newtype种类等价物？

我已经发现我可以使用类型族来获得类似的东西：

{-# LANGUAGE TypeFamilies #-}
data Inf (x :: * -> *) = Inf
type family RunInf x :: * -> *
type instance RunInf (Inf x) = x

但我对这个解决方案不满意 - 与等效类型不同，Inf 不会创建新种类（Inf x 有种类 *），所以有不太安全。

这个问题有更优雅的解决方案吗？

Answer 1

我认为您正在寻找 Fix，它被定义为

data Fix f = Fix (f (Fix f))

Fix 为您提供 f 类型的定点。我不确定您要做什么，但是当您使用递归方案（您可以使用的递归模式）时，通常会使用这种无限类型，请参阅 Edward Kmett 的 recursion-schemes 包或使用免费的单子，其中包括things 允许您以单子样式构建 AST。

Answer 2

回应：

Like recursion-schemes, I want a way to construct ASTs, except I want my ASTs to be able to refer to each other - that is a term can contain a type (for a lambda parameter), a type can contain a row-type in it and vice-versa. I'd like the ASTs to be defined with an external fix-point (so one can have "pure" expressions or ones annotated with types after type inference), but I also want these fix-points to be able to contain other types of fix-points (just like terms can contain terms of different types). I don't see how Fix helps me there

我有一个方法，可能接近您的要求，我已经 experimenting with。它似乎非常强大，尽管围绕这个结构的抽象需要一些开发。关键是有一种 Label 表示递归将从哪里继续。

{-# LANGUAGE DataKinds #-}

import Data.Kind (Type)

data Label = Label ((Label -> Type) -> Type)
type L = 'Label

L只是构造标签的捷径。

开定点定义属于 (Label -> Type) -> Type 类型，也就是说，它们采用 "label interpretation (type) function" 并返回一个类型。我称这些为"shape functors"，并用字母h抽象地指代它们。最简单的形状函子是不递归的：

newtype LiteralF a f = Literal a  -- does not depend on the interpretation f
type Literal a = L (LiteralF a)

现在我们可以做一个小的表达式语法作为例子：

data Expr f
    = Lit (f (Literal Integer))
    | Let (f (L Defn)) (f (L Expr))
    | Var (f (L String))
    | Add (f (L Expr)) (f (L Expr))

data Defn f
    = Defn (f (Literal String)) (f (L Expr))

注意我们如何将 labels 传递给 f，后者负责关闭递归。如果我们只想要一个普通的表达式树，我们可以使用 Tree:

data Tree :: Label -> Type where
    Tree :: h Tree -> Tree (L h)

然后 Tree (L Expr) 与您期望的正常表达式树同构。但这也允许我们，例如，在树的每一层用标签相关的注释来注释树：

data Annotated :: (Label -> Type) -> Label -> Type where
    Annotated :: ann (L h) -> h (Annotated ann) -> Annotated ann (L h)

在回购中 ann 由形状仿函数而不是标签索引，但现在对我来说这似乎更清晰。有很多像这样的小决定要做出，我还没有找到最方便的模式。围绕形函子使用的最佳抽象仍然需要探索和开发。

还有很多其他的可能性，其中很多我还没有探索过。如果您最终使用它，我很想听听您的用例。

Answer 3

对于数据种类，我们可以使用常规的新类型：

import Data.Kind (Type)

newtype Inf = Inf (Inf -> Type)

并推广它（使用 '）以创建新种类来表示循环：

{-# LANGUAGE DataKinds #-}

type F x = x ('Inf x)

对于解压其 'Inf 参数的类型，我们需要一个类型系列：

{-# LANGUAGE TypeFamilies #-}

type family RunInf (x :: Inf) :: Inf -> Type
type instance RunInf ('Inf x) = x

现在我们可以用新的种类来表达无限种类，所以不会丢失种类安全。

感谢@luqui 指出他回答中的 DataKinds 部分！

表达无限种

Expressing infinite kinds

haskell

types

type-families

type-kinds