gpt4 book ai didi

haskell - 使用 Hindley Milner 和约束​​推断递归表达式

转载 作者:行者123 更新时间:2023-12-02 04:49:41 26 4
gpt4 key购买 nike

我试图推断以下表达式的类型:

let rec fix f = f (fix f)

应指定类型(a -> a) -> a

使用自下而上算法(在概括hindley-milner类型推理算法中描述)并添加以下规则后:

           a1, c1 |-BU e1 : t1     B = fresh var
---------------------------------------------------------
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t

我剩下以下类型:t1 -> t2

以及以下约束:

t0 = fix
t1 = f
t2 = f (fix f)
t3 = f
t4 = fix f
t5 = fix
t6 = f

t3 = t1
t3 = t4 -> t2
t5 = t0
t5 = t6 -> t4
t6 = t1

我看不出如何解决这些约束,以至于我只剩下类型 (a -> a) -> a。我希望有人能明显看出我是否出错了。

full source code here

最佳答案

第一个修复f不应该有一个t7吗?这些给出了约束:

t7 = t2
t0 = t1 -> t7

从中您应该能够推断出 t4 = t2,然后推断出 t0 = (t2 -> t2) -> t2

关于haskell - 使用 Hindley Milner 和约束​​推断递归表达式,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/10575268/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com