Are there any other HOL programming languages ​​besides Caledon based on haskell?

Question

There are programming languages ​​and theoretical evidence based on higher order logic (HOL). Examples include Twelf , lambda proog , Isabelle . For example, Twelf is both a programming language and a theoretical breakthrough, while Isabelle is basically a theoretical breakthrough, but code is available for extracting Isabelle.

I am looking for a haskell-based HOL programming language. The reason is that I like, for example, lambda proog very much, but that does not mean that it is a practical programming language. The Lambda prologue does not have a standard library and interacting with external libraries does not seem trivial. The problem is that if you need some kind of functionality, for example, writing a parser for a text file, you cannot interact, say, with many available existing libraries for haskell, and there is also no standard library, so you start from scratch .

Today I came across the Caledon programming language, which was implemented as a master's thesis. On github page:

Caledon is a typically typed, polymorphic higher order logic of a programming language.

This is interesting because it is written in haskell, so it is easy to extend and interact with existing haskell libraries. But it seems that the project is at an early stage, I'm not sure that the input / output (IO) function is implemented. Since I only found out about Caledon today, I think I might have missed some other projects. (BTW, I'm not interested in standard logic programming languages ​​like prolog).

Are there programming languages ​​based on higher-order logic other than Caledon that are implemented in haskell?

(I ask for "implement in haskell" because it’s pretty easy to connect programming languages ​​that can be extracted or implemented in haskell. For example, the Agda programming language can be compiled into haskell code, and haskell libraries can be conveniently used and it is extremely easy to use haskell libraries, if you know how to do this, many other programming languages ​​(like ATS) that I believe provide only the smallest common denominator, which is the interface of an external C-based function (FFI). of the two higher programming languages ​​through their corresponding C-based FFI interface. Thus, the seemingly incorrect part that “should be implemented in haskell.” Also, as a side note, some users in the past referred to my description of Agda as a programming language, but of course this is not true, i.e. consider Curry-Howard )

Answer 1

"Haskabelle is a converter from Haskell source files to Isabelle / HOL theory implemented in Haskell itself."

Haskabelle

Answer 2

short answer: I do not know. long answer: you have a small chance that you will find a purely academic language with thousands of libraries and tools for it. if for some reason you need this particular language for a particular problem, then use it ONLY for this problem. not for parsing files, calculating taxes, or launching rockets. create libraries and link them to other programs. or even better: create a microservice or connect programs in another way (for example, standard input / output), which does not require much effort. always use the best tool for the job

Answer 3

Strange statement: Haskell is a higher-order logical programming language based on Haskell. Type inference in Haskell with multi-parameter class types, family types, unsolvable inference, and what actually constitutes a higher order logical programming language. This probably won't help you much, because:

• The spectrum is literally constantly changing (I had several packages compatible with crashes, because they were based on hacks that received a “fix”).
• The type system itself does not have IO (yet?)
• It cannot really call other Haskell libraries from type inference
• Not very fast.
• The semantics of logical programming are not entirely clear or stable.
• This does not allow you to combine with lambdas or other types of classes, although it does allow you to combine functions.

Unfortunately, I know unusually few complete HOL languages, not to mention the ones implemented in Haskell - it turns out that higher-level unification is a huge pain for implementation.