定义具有最少定点,总和和产品类型的列表

Question

我想仅使用此类型定义来定义列表:

data Unit = Unit
data Prod a b = P a b
data Sum a b = L a | R b
newtype Mu f = Mu (forall a . (f a -> a) -> a)

我成功地定义了自然数如下:

zeroMu = Mu $ \f -> f $ L Unit
succMu (Mu g) = Mu $ \f -> f $ R $ g f

我知道如何借助额外的数据类型定义列表:

data ListF a x = NilF | ConsF a x
nilMu' = Mu $ \f -> f $ NilF
consMu' x (Mu g) = Mu $ \f -> f $ ConsF x $ g f

我能得到的'更好'就是这个,但它没有类型检查(预期类型是μL.(1+(a*L))):

nilMu = Mu $ \f -> f $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ R $ P x $ g f

如何定义nilMu和consMu使用以前定义的类型及其构造函数？

编辑

正如@chi回答所解释的那样,可以定义newtype如下:

newtype F a x = F (Sum Unit (Prod a x))
nilMu = Mu $ \f -> f $ F $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ F $ R $ P x $ g f

它进行类型检查,但需要定义新类型.

这个问题的目的是扩展一个简单类型的组合逻辑,包括单元,乘积,求和和递归类型.第一三种类型是直接实现引入7个新组合子(unit,pair,first,second,left,right,case).递归类型似乎也很容易实现,只需添加一个类型构造函数组合器mu,但是这个questoins显示的不够灵活,没有其他语言结构.

有这个问题的解决方案吗？是否存在具有递归类型的组合逻辑以供参考？

Answer 1

如果没有额外的,data或者newtype在Haskell中,你不能这样做.

要做到这一点,人们需要写

nilMu :: Mu (\l -> S (P a l) ())
consMu :: a -> Mu (\l -> S (P a l) ()) -> Mu (\l -> S (P a l) ())

但是Haskell不允许以这种方式使用类型级函数.Mu只能应用于类型的类型构造函数* -> *,而不能应用于同类型的类型级函数.

nilMu :: Mu (F a)
consMu :: a -> Mu (F a) -> Mu (F a)

where F a定义为附加类型

newtype F a x = F (S (P a x) ())

由于Haskell不允许类型级函数的原因,请考虑

assuming foo :: f a -> f Char
infer    foo True :: ???

有人可能会说,在foo True,True是Bool,所以我们可以推断f = \t->t和a = Bool.结果是foo True :: (\t->t) Char = Char.

人们可能会认为,我们可以推断f = \t->Bool和a = String,那结果是foo True :: (\t->Bool) Char = Bool

一般来说,我们不喜欢这样.我们希望通过模式匹配f和a实际类型来进行类型推断.为此,我们想要两者f并且在实际类型中a具有相应的"明显" 名称.

对于它的价值,您可以在依赖类型语言中执行此操作,例如Coq,Agda,Idris等.在那里,类型推断不适用于foo True上面的代码,因为f无法推断.更糟糕的是,在这些语言中,如果bar :: f a -> ...我们打电话bar [True],那么f可能无法推断,[]因为这不是唯一的解决方案(尽管它们确实具有良好的启发式,但无论如何通常都会起作用,即使一般问题是不可判定的).