Yup! This is more to do with a very specific part of type theory - ie. 'type reconstruction' (more commonly referred to as 'type inference'). One of the most notable examples of this is the so-called 'Hindley-Milner type system' which can be proven to decidable. Here is a good explanation of the constraint-solving algorithm: http://jozefg.bitbucket.org/posts/2015-02-28-type-inference....

[1] http://eclipseclp.org/doc/embedding/embroot.html

https://code.google.com/archive/p/pyswip/

It's a bit unstable but if you really, really want to embed Swi Prolog it's available as a .dll - which is how pyswip and all other foreign language interfaces work.

There is: types are pattern that data must conform to (and operations also- so, data). To declare a value "x" as having the type "int" is to assert that "x" matches whatever pattern "int" stands for.

The connection to logic programming is that logic programming languages, certainly Prolog, are implemented as relational databases with a search procedure using pattern matching to find relations that conform to the pattern of a query. The pattern matching algorithm in Prolog is called unification: it's like the pattern matching in regular expressions, only Turing complete, so it can represent any program. In fact, Prolog programs are patterns representing themselves [1]. But let's not get too excited.

Prolog's pattern matching makes it indeed very convenient for representing types, even complex types and nested hierarchies of such. For example, Haskell uses something very similar to unification for its type inference system [2].

However- a word of caution. Doing simple type inference ish is not that complicated in Prolog (at least if you're doing it as an exercise- doing it industrial-strength would take a lot of effort). Doing something more complicated, like representing Hindley-Milner like in [3], is more of an undertaking, which is (partly) why Prolog itself doesn't have any types in the conventional sense. Then again predicates with implicitly universally quantified variables are themselves types, er, implicitly, so in a way each Prolog program declares its own type system exactly matching itself.

See [4] for a discussion of logic progamming, types and category theory (I'm not affiliated with the author in any way).

_______________

[1] https://en.wikipedia.org/wiki/Homoiconicity#Homoiconicity_in...

[2] https://wiki.haskell.org/Type_inference

[3] http://www.swi-prolog.org/pack/list?p=type_check

[4] http://www.drdobbs.com/what-might-category-theory-do-for-art...

The link Kiselyov mentions is between Garbage collection (-ish, really it's more lifetime analysis a la Rust) and when it is appropriate to generalise a free type variable and how they both interact with aliasing. Take the following expression:

    fun (x) let y = x in y

* It has type `forall 'a . 'a -> 'a` (Keeping the universal quantification explicit).

* The value held in `y` outlives the scope of `y`, because it is aliased in `x`.

But the naïve solution results in:

* The type `forall 'a 'b . 'a -> 'b` (Any function of this type is pure sorcery)

* The value of `y` (and `x`) gets deallocated at the end of `y`'s scope.

The solution is that each type variable should keep track of the scope it was introduced in (like de Bruijn indices), and when generalising, we only universally quantify variables at more deeply nested scopes (which corresponds to deallocating unreachable things).

Of the proprietary Prologs I've mostly worked with Sicstus which was the fastest one I've used and had pretty good constraint libraries. It also has a lot of extra features (logical loops etc.) but I mostly used it for legacy reasons and generally prefer a free implementation (for any programming language).

I've heard good things about Eclipse (unfortunate naming, hard to search for) when it comes to constraint programming.

Some random observations: It usually takes my brain a bit to switch to "Prolog mode". You can build some fairly elegant things (constraint based poker hand rankings was the last thing I built) but it's usually not very fast. However I'm not a very proficient Prolog programmer so it could very well be on me for not optimizing enough. If you want some book recommendations I think the best first book is "Prolog Programming for Artificial Intelligence" (best intro section which is the first half of the book so highly recommended even if you don't care about AI at all). The classics are great followups to that (Art of Prolog first, Craft of Prolog second).

I recall this paper, by Joe Armstrong of Erlang... I'll have to go read it again.

"Use of Prolog for developing a new programming language"

https://scholar.google.com/scholar?cluster=23466104209097450...

Hm after scanning it, I think the reason I never really got it the first time around is that I don't know Prolog :) Might be time to fix that.

What turned me off to Prolog is that there's no way to reason about the computational complexity of the algorithm. Declarative languages often have this problem. That's why you have SQL queries that literally take thousands of times longer than a Python script in production (hours vs seconds). Programming models also need performance models.

Reasoning about performance is quite possible; there's good advice in Richard O'Keefe's The Craft of Prolog.

[Edit: fixed the book title, thanks to a friendly correction. The Practice of Prolog is a different book, also good, but less relevant.]

There are real tutorials on DCGs available, e.g.

http://www.pathwayslms.com/swipltuts/dcg/

(BTW, SWI-Prolog, which the tutorial uses, is freely available here:

http://www.swi-prolog.org/ )

http://www.mtome.com/Publications/PNLA/prolog-digital.pdf

And there's a set of course materials in HTML for "Natural Language Processing in Prolog", a course at Union College in Schenectady, NY by Patrick Blackburn and Kristina Striegnitz that seems worthwhile:

http://cs.union.edu/~striegnk/courses/nlp-with-prolog/html/t...

That's easy to figure out once you realise your code also has an imperative reading. So for instance it's obvious that reversing a list:

  reverse(A, B) :-
        reverse(A, [], B, B).

  reverse([], A, A, []).
  reverse([B|A], C, D, [_|E]) :-
        reverse(A, [B|C], D, E).

Or, for instance, say you wanted to apply reverse/4 to elements of a list-of-lists:

  findall(L_, (member(L, Ls), reverse(L, L_)), Ls_).

  revall(Ls, Ls_):-
       revall(Ls, [], Ls_).

  revall([], Ls, Ls_):-
        reverse(Ls, Ls_)
        ,!.
  revall([L|Ls],Acc,Bind):-
         reverse(L, L_)
         ,revall(Ls, [L_|Acc], Bind).

Logic programming seems to be like monads, either you get it or not, but it is hard to explain to others.

Prolog and Lisp were the two languages we were forbidden to use in compiler design project, as it was considered "cheating" versus using something harder like C.

"Cheating"? Smells like a chance for the revenge of the pattern-matching metacompiler!

feels like lego where prolog is duplo.

The implementation and ecosystem are quite far from something like Python, of course, but it does look like the most beautiful house in the street to me when you just walk past it.

Except for things like the system described in the featured article, where the unique strength of Prolog is the ability to pass around partially instantiated data structures and use full unification. Last time I checked, Mercury still insisted that terms be ground (or completely free variables), which means that for this kind of problem you don't gain much from its flavor of logic programming :-(

Haskell/Ocaml/SML? :3

Haskell was still not a thing our department cared about, although we got to read some stuff about Miranda.

SML was never a thing at our university.

The website text (free) is the first edition of the book; the authors have also published a second edition with updates.

These deficiencies are clearly visible in Lisps where you're given great meta-power with macros, but where the type system starts fighting petulantly, whenever one wants to do something fast. In this respect C++ templates are much better.

Shen on the other hand seems quite interesting (and seems to come with its own prolog engine!); anyone here have any views on this Lisp ?

Shen implemented Prolog to build it's type checker with.

The type systems I've seen for dependantly typed languages have mostly tried to use traditional formal logic syntax, with resulting usability issues and frequently a mismatch with the programming language.

For example, ATS is based on ML syntax, but the typing frequently results in functions of the form:

    fun foo =
      let _ = ...
          x = ...
          _ = ...
      in
        ()

You haven't really explained what your idea is or how Prolog differs from "traditional formal logic syntax". If anything, Prolog's predicate syntax is closer to formal logic than the many ML-based dependently typed programming languages; except that quantifiers are implicit in Prolog.

Anyway, you might want to look around http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ and espectially http://www.lix.polytechnique.fr/~dale/lProlog/

> requently a mismatch with the programming language

I find Coq's syntax fairly regular in this regard. (The syntax for expressing computations and predicates, not the tactic and tactical syntaxes.)

> So, why not use a programming language for type-level programming?

Because of the "mismatch with the programming language" that you yourself have identified as a problem.

Whenever someone asks where to "widen their view" I generally recommend prolog or factor (15 years ago, I would have said scheme, but lisps seem to have been all the rage so I no longer need to).

Scheme/Lisp is about how data and code are equivalent in a practical sense.

I'm not sure how I would describe Prolog in a single sentence - it's about using a powerful concept (Unification) as a base of computation - it makes a lot of logic programming simple (and unfortunately, it makes some simple iteration complicated).

Forth is an exercise in minimalism and blurring (or actually removing) the line between compiling, interpreting, parsing. I wouldn't treat Forth and Factor equivalently - Factor borrows Forth's concatenativeness, but it is very far from Forth's minimalism.

K is an exercise in choosing the minimal set of operators and functions that would produce very terse programs that need much less abstraction, without having to compromise on speed. Unlike Lisp and Forth, the base K has some 50-100 mostly orthogonal operators (depending on how you count) that work together to give you a lot without forcing you to abstract.

Not the OP here, but I'll give it a partial shot. The power of Forth comes from its extremely simple syntax and the ways you can extend it. A Forth program is just a sequence of "words", which are any sequences of non-whitespace characters separated by whitespace. Users can define new words. These can be "parsing words" which can consume the input that follows them in arbitrary ways.

So, for example, given appropriate definitions, this is a valid Forth program:

    ax bx mov             \ mov ebx,eax
    3 # ax mov            \ mov eax,3

Or, given appropriate definitions, this is a valid Forth program:

    select * from customers

All that said, it's ugly and complex and I always find it difficult to figure out what's going on with all the strangely named concepts and compile-time effects and run-time effects of everything. But still. Interesting stuff.