时间戳

首页 > 解决方案 > “模式匹配”并递归封闭类型族中的类型以进行类型相等证明

haskell - “模式匹配”并递归封闭类型族中的类型以进行类型相等证明

问题描述

假设这样的情况：

data Foo a = Foo

type family AlwaysInt a where
  AlwaysInt (Foo a) = AlwaysInt a
  AlwaysInt _       = Int

我想证明AlwaysInt a永远是Int。

import Data.Type.Equality

lemma :: AlwaysInt a :~: Int
lemma = undefined

我如何证明这一点？我想对类型族定义中的每种类型进行“模式匹配”，因为我可以证明每种情况的引理，但是我该如何进行这样的模式匹配呢？

丑陋的解决方法是添加一个a参数lemma并离开undefined那里或放置一条error消息，但这在现实生活中并不是很好。

编辑：忘记实际问题

标签： haskelltype-families

解决方案

你无法证明这一点。

type family Any where {}
type family ManyFoo where
  ManyFoo = Foo ManyFoo

是什么AlwaysInt Any？Any是一个卡住的类型，所以 GHC 将无法减少类型族应用。

是什么AlwaysInt ManyFoo？嗯，ManyFoo是无限类型，

ManyFoo = Foo (Foo (Foo ...))

所以 GHC 会进入一个无限循环，试图计算它或试图计算AlwaysInt ManyFoo.

推荐阅读