有基于高阶逻辑（HOL）的编程语言和定理证明器 . 示例包括Twelf，lambda prolog，Isabelle . 例如，Twelf既是编程语言又是定理证明者，而Isabelle主要是一个定理证明者，但是对于Isabelle代码提取是可用的 .
我正在寻找一种基于haskell的HOL编程语言 . 原因是我非常喜欢lambda prolog，但它并不是一种实用的编程语言 . Lambda prolog缺少标准库，与外部库的接口似乎并不简单 . 问题是如果你需要一些功能，比如为文本文件编写解析器，你就不能与haskell的许多可用现有库接口，而且，没有标准库，所以你从头开始 .
今天我看到了Caledon编程语言，它被实现为硕士论文 . 从github页面：
Caledon是一种依赖类型，多态，高阶逻辑编程语言 .
这很有趣，因为它是用haskell编写的，所以它应该很容易扩展并与现有的haskell库接口 . 但似乎该项目处于初期阶段，我不确定是否实现了输入输出（IO） . 由于我今天才了解卡利多，我想我可能错过了一些其他项目 . （顺便说一句，我对像prolog这样的标准逻辑编程语言不感兴趣） .
除了Caledon之外，是否有基于高阶逻辑的编程语言在haskell中实现？
（我要求"implemented in haskell"，因为连接可以提取到haskell或在haskell中实现的编程语言相当容易 . 例如，Agda编程语言可以编译为haskell代码，haskell库可以方便地使用，并且非常容易如果你知道如何使用haskell库 . 我相信的许多其他编程语言（例如，ATS）只提供最小的公共分母，它是基于C的外部函数接口（FFI） . 在我看来，连接两种更高级的编程语言是相当麻烦的通过他们各自的基于C的FFI界面 . 因此，这个似乎是abitrary部分"it should be implemented in haskell" . 此外，作为旁注，一些用户过去曾因为我将Agda描述为编程语言而被投票，但当然这不是真的，即，考虑Curry-Howard）
3 回答
“Haskabelle是一个从Haskell源文件转换为在Haskell本身实现的Isabelle / HOL理论的转换器 . ”
Haskabelle
简短的回答：我不知道 . 答案很长：你很少有机会找到纯数学的语言，有成千上万的图书馆和工具 . 如果由于某种原因您需要针对某些特定问题的特定语言，那么仅将其用于该问题 . 不是解析文件，计算税收或发射火箭 . 创建库并将其与其他程序链接 . 甚至更好：创建微服务或以其他方式连接程序（例如标准输入/输出），这不需要太多努力 . 总是使用最好的工具来完成工作
Strange Statement: Haskell ' is a higher order logic programming language based on Haskell. Type inference in Haskell with multiparameter type classes, type families, undecidable inference and whatnot actually forms a higher order logic programming language. This probably doesn' t非常有帮助，因为：
规范实际上在不断变化（我有一些软件包松散的兼容性，因为它们基于hacks得到"fixed"）
类型系统本身没有IO（还是？）
它无法从类型推断中真正调用其他Haskell库
它不是很快 .
逻辑编程语义不完全清晰或稳定 .
它不允许您与lambdas或其他类型类统一，尽管它允许与函数统一 .
可悲的是，我知道非常少的完全HOL语言，更不用说在Haskell中实现的语言 - 事实证明，更高阶的统一是一个巨大的痛苦 .