4 ms·

Writing custom type systems for Python in Prolog

125 points by type0 10y ago

deleted 10y ago
[deleted]
bobsh 10y ago
The definition of Standard ML is perhaps where the OP might like to look, for a somewhat more advanced example.
bjz_ 10y ago
> Everybody who does PL theory more seriously probably knows that, but I didn't realize how close type inference and prolog-like systems look. 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.html http://jozefg.bitbucket.org/posts/2015-02-28-type-inference....
- malisper 10y ago
  Algorithm W, the algorithm used to do type inference in Hindley Milner is effectively just unification (the process by which Prolog infers facts, as mentioned in the post you referenced), applied to types.
  - bjz_ 10y ago
    Yeah - should have been more clear on that ;)
- baq 10y ago
  I've looked at Prolog for implementing a rule-based workflow system, but I find that it's very hard to embed eg. SWI Prolog into Python, in which the rest of the project is written. Does anyone know of an embeddable Prolog, preferably open source?
  - YeGoblynQueenne 10y ago
    Swi Prolog has an interface to python, pyswip: https://code.google.com/archive/p/pyswip/ 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.
  - junke 10y ago
    ECLiPSe, for example. See [1] for documentation about how to embed it. However, this is targetted at C, Java and Tcl/Tk, not Python. Another approach is to use a client/server approach with two processes (python starts a background prolog, for example). [1] http://eclipseclp.org/doc/embedding/embroot.html http://eclipseclp.org/doc/embedding/embroot.html
  - sitkack 10y ago
    Could you abstract it out as a network service?
qwertyuiop924 10y ago
This has singlehandedly made me interested in learning more about prolog. I mean, if you can do things like that that simply... Holy crap. No wonder so many lisps incude a prolog implementation of some sort.
- coliveira 10y ago
  Prolog was designed to do this kind of things easily. You can parse languages with easy, and perform all kinds of programming transformations that would take thousands of lines in other languages in just a few rules. The problem with prolog is when you try to do the run-of-the-mill stuff. Not because it is impossible or even hard, but because you need to change the way you think about programming. This is very difficult for programmers that are already used to imperative languages.
  - chubot 10y ago
    Really, how does it handle parsing? What kind of languages can you parse? 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=2346610420909745067&hl=en&as_sdt=0,5&sciodt=0,5 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.
    - abecedarius 10y ago
      https://en.wikipedia.org/wiki/Definite_clause_grammar https://en.wikipedia.org/wiki/Definite_clause_grammar -- parsing in Prolog. As usual with Wikipedia on technical topics it looks like a poor introduction, sorry. 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.]
YeGoblynQueenne 10y ago
>> Is there a deeper link between logical programming and type theory? 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_Prolog https://en.wikipedia.org/wiki/Homoiconicity#Homoiconicity_in... [2] https://wiki.haskell.org/Type_inference https://wiki.haskell.org/Type_inference [3] http://www.swi-prolog.org/pack/list?p=type_check http://www.swi-prolog.org/pack/list?p=type_check [4] http://www.drdobbs.com/what-might-category-theory-do-for-artifi/228700165 http://www.drdobbs.com/what-might-category-theory-do-for-art...
- __s 10y ago
  Gankro cites niko as saying Rust trait resolution is basically prolog: https://news.ycombinator.com/item?id=11781923 https://news.ycombinator.com/item?id=11781923 (wish he'd cite with a link)
- agumonkey 10y ago
  Ocaml type inference has subtle variations on this I believe, according to kiselyov it links GC and TC http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html
ittekimasu 10y ago
Sweet! I've always wished a better type systems were available in dynamic languages. 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 ?
- bjz_ 10y ago
  Also be sure to check out typed racket!
  - jakub_h 10y ago
    Sadly, Typed Racket always seemed to me like some kind of shoehorning an ad-hoc system onto an AST. For that purpose, a deductive system seems much more natural. There may be problems with decidability, but the fortuitous thing is that this is not a deal-breaker for a primarily dynamic language. You should always be able to rewrite your modules so that they're easier to check, but even if you can't do that outright, the system could still find faster versions if a few type guards or other invariant checks get inserted here and there, or perhaps some form of assistant in your development environment could hint at the need to insert them manually.
- qbrass 10y ago
  >Shen on the other hand seems quite interesting (and seems to come with its own prolog engine!) Shen implemented Prolog to build it's type checker with.
mcguire 10y ago
Anyone have any thoughts on an idea I've been pondering for a while: Prolog as the type system for dependant typing? 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 () So, why not use a programming language for type-level programming?
- tom_mellior 10y ago
  > Anyone have any thoughts on an idea I've been pondering for a while: Prolog as a type system [...] traditional formal logic syntax, with resulting usability issues 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/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ and espectially http://www.lix.polytechnique.fr/~dale/lProlog/ 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.
Johnny_Brahms 10y ago
In my programming career 3 languages have changed how I look at programming. The first one was scheme which is still my go to language for most of my personal projects. The second one was prolog and the third was Forth/factor. 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).
- zem 10y ago
  i think ML has changed the way i look at programming more than anything else. pattern matching over algebraic datatypes is a very powerful way to think about modelling something as code even if your language doesn't support either feature. (to paraphrase ashley yakeley, "every sufficiently well-documented lisp program contains an ML program in its comments")
- beagle3 10y ago
  I have these three in my list, and one more: APL (or J or K -- especially K) 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.
- bogomipz 10y ago
  Can you elaborate on what is special about Forth? I see Forth articles show up on HN now and again but I've been able to glean why its special to so many. I know its been around forever.

125 points by type0 10y ago

deleted 10y ago

[deleted]

bobsh 10y ago

The definition of Standard ML is perhaps where the OP might like to look, for a somewhat more advanced example.

bjz_ 10y ago

> Everybody who does PL theory more seriously probably knows that, but I didn't realize how close type inference and prolog-like systems look. 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.html http://jozefg.bitbucket.org/posts/2015-02-28-type-inference....

malisper 10y ago
Algorithm W, the algorithm used to do type inference in Hindley Milner is effectively just unification (the process by which Prolog infers facts, as mentioned in the post you referenced), applied to types.
- bjz_ 10y ago
  Yeah - should have been more clear on that ;)
baq 10y ago
I've looked at Prolog for implementing a rule-based workflow system, but I find that it's very hard to embed eg. SWI Prolog into Python, in which the rest of the project is written. Does anyone know of an embeddable Prolog, preferably open source?
- YeGoblynQueenne 10y ago
  Swi Prolog has an interface to python, pyswip: https://code.google.com/archive/p/pyswip/ 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.
- junke 10y ago
  ECLiPSe, for example. See [1] for documentation about how to embed it. However, this is targetted at C, Java and Tcl/Tk, not Python. Another approach is to use a client/server approach with two processes (python starts a background prolog, for example). [1] http://eclipseclp.org/doc/embedding/embroot.html http://eclipseclp.org/doc/embedding/embroot.html
- sitkack 10y ago
  Could you abstract it out as a network service?

qwertyuiop924 10y ago

This has singlehandedly made me interested in learning more about prolog. I mean, if you can do things like that that simply... Holy crap. No wonder so many lisps incude a prolog implementation of some sort.

coliveira 10y ago
Prolog was designed to do this kind of things easily. You can parse languages with easy, and perform all kinds of programming transformations that would take thousands of lines in other languages in just a few rules. The problem with prolog is when you try to do the run-of-the-mill stuff. Not because it is impossible or even hard, but because you need to change the way you think about programming. This is very difficult for programmers that are already used to imperative languages.
- chubot 10y ago
  Really, how does it handle parsing? What kind of languages can you parse? 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=2346610420909745067&hl=en&as_sdt=0,5&sciodt=0,5 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.
  - abecedarius 10y ago
    https://en.wikipedia.org/wiki/Definite_clause_grammar https://en.wikipedia.org/wiki/Definite_clause_grammar -- parsing in Prolog. As usual with Wikipedia on technical topics it looks like a poor introduction, sorry. 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.]

YeGoblynQueenne 10y ago

>> Is there a deeper link between logical programming and type theory? 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_Prolog https://en.wikipedia.org/wiki/Homoiconicity#Homoiconicity_in... [2] https://wiki.haskell.org/Type_inference https://wiki.haskell.org/Type_inference [3] http://www.swi-prolog.org/pack/list?p=type_check http://www.swi-prolog.org/pack/list?p=type_check [4] http://www.drdobbs.com/what-might-category-theory-do-for-artifi/228700165 http://www.drdobbs.com/what-might-category-theory-do-for-art...

__s 10y ago
Gankro cites niko as saying Rust trait resolution is basically prolog: https://news.ycombinator.com/item?id=11781923 https://news.ycombinator.com/item?id=11781923 (wish he'd cite with a link)
agumonkey 10y ago
Ocaml type inference has subtle variations on this I believe, according to kiselyov it links GC and TC http://okmij.org/ftp/ML/generalization.html http://okmij.org/ftp/ML/generalization.html

ittekimasu 10y ago

Sweet! I've always wished a better type systems were available in dynamic languages. 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 ?

bjz_ 10y ago
Also be sure to check out typed racket!
- jakub_h 10y ago
  Sadly, Typed Racket always seemed to me like some kind of shoehorning an ad-hoc system onto an AST. For that purpose, a deductive system seems much more natural. There may be problems with decidability, but the fortuitous thing is that this is not a deal-breaker for a primarily dynamic language. You should always be able to rewrite your modules so that they're easier to check, but even if you can't do that outright, the system could still find faster versions if a few type guards or other invariant checks get inserted here and there, or perhaps some form of assistant in your development environment could hint at the need to insert them manually.
qbrass 10y ago
>Shen on the other hand seems quite interesting (and seems to come with its own prolog engine!) Shen implemented Prolog to build it's type checker with.

mcguire 10y ago

Anyone have any thoughts on an idea I've been pondering for a while: Prolog as the type system for dependant typing? 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 () So, why not use a programming language for type-level programming?

tom_mellior 10y ago
> Anyone have any thoughts on an idea I've been pondering for a while: Prolog as a type system [...] traditional formal logic syntax, with resulting usability issues 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/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ and espectially http://www.lix.polytechnique.fr/~dale/lProlog/ 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.

Johnny_Brahms 10y ago

In my programming career 3 languages have changed how I look at programming. The first one was scheme which is still my go to language for most of my personal projects. The second one was prolog and the third was Forth/factor. 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).

zem 10y ago
i think ML has changed the way i look at programming more than anything else. pattern matching over algebraic datatypes is a very powerful way to think about modelling something as code even if your language doesn't support either feature. (to paraphrase ashley yakeley, "every sufficiently well-documented lisp program contains an ML program in its comments")
beagle3 10y ago
I have these three in my list, and one more: APL (or J or K -- especially K) 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.
bogomipz 10y ago
Can you elaborate on what is special about Forth? I see Forth articles show up on HN now and again but I've been able to glean why its special to so many. I know its been around forever.