代码之家 › 专栏 › 技术社区 › yairchu

表示无限类

type-kinds type-families types haskell

7

yairchu · 技术社区 · 6 年前

在haskell中表示无限类型时:

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

可以使用 newtype 要做到这一点:

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

f x = x (Inf x)

有没有 新型 等价于可以表示无限类的类型?

我已经发现我可以用类型族来得到类似的东西:

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

但我对这个解决方案不满意-不同于同等类型, Inf 不会创造一种新的( Inf x 有这种 * )所以安全性比较差。

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

3 回复 | 直到 6 年前

1

4

luqui 6 年前

回复:

与递归方案一样,我希望有一种方法来构造AST,但我希望我的AST能够相互引用-也就是说,术语可以包含类型(对于lambda参数),类型可以包含行类型,反之亦然。我希望用一个外部固定点定义AST(这样一个可以有“纯”表达式或在类型推断后用类型注释的表达式),但我也希望这些固定点能够包含其他类型的固定点(就像术语可以包含不同类型的术语一样)。我不知道Fix是如何帮助我的

我有一个方法,可能接近你的要求,我已经 experimenting with . 虽然围绕这个结构的抽象需要一些开发,但它似乎非常强大。关键是有一种 Label 它指示递归将从何处继续。

{-# LANGUAGE DataKinds #-}

import Data.Kind (Type)

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

L 只是构建标签的快捷方式。

开放不动点定义是一种 (Label -> Type) -> Type 也就是说,它们采用“标签解释(类型)函数”并返回类型。我称之为“形状函数”,抽象地用字母来指代它们。 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))

注意我们是怎么通过的标签到 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 是由形状函数而不是标签索引的,但现在我觉得这更清楚了。有很多这样的小决定要做,我还没有找到最方便的模式。围绕形状函数使用的最佳抽象仍然需要探索和开发。

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

2

yairchu 6 年前

对于数据类型,我们可以使用常规newtype:

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 参与他的回答!

3

1

madgen 6 年前

我想你在找 Fix 定义为

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

固定 给你类型的固定点 f . 我不确定您要做什么,但是当您使用递归权值(您可以使用的递归模式)时,通常会使用这种无限类型,请参见 recursion-schemes 由Edward Kmett或免费Monads提供的包,除其他外,它允许您以一元风格构建ASTS。