6 ms·

New rule. Any sufficiently advanced type system is an ad-hoc re-implementation of Prolog. Once you have unification and backtracking you basically have Prolog a

by _qc3o 10y ago

New rule. Any sufficiently advanced type system is an ad-hoc re-implementation of Prolog. Once you have unification and backtracking you basically have Prolog and can implement whatever Turing machine you want with the type system.

badtuple 10y ago
Here's a great article about making the Prolog re-implementation in Rust's type system less ad-hoc and more awesome: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/ http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowe... The best days are when Niko posts about his work on Rust. Always interesting and they often exploit the power behind ideas like "It's basically Prolog" instead of apologizing for it. It's exciting and the kind of thinking that makes me remember why I fell in love with programming in the first place.
therein 10y ago
I read that with Bill Maher's voice in my head.
ruricolist 10y ago
Alternatively, you could just use Shen, which actually uses Prolog to implement its type system.
- dkarapetyan 10y ago
  Ya but for some reason Shen uses weird sequent calculus syntax. I'd much rather write Prolog rules than sequents.
- throwaway7645 10y ago
  Is the license for Shen still odd? I know Tarver doesn't believe in free software.
  - mcbits 10y ago
    There is this page suggesting it's mostly BSD, but the License link is a 404: http://shenlanguage.org/ethics.html http://shenlanguage.org/ethics.html
lomnakkus 10y ago
If only. Prolog is actually reasonably pleasant to program in. Accidentally Turing Complete type systems are usually not all that pleasant in practice. Examples: C++ Templates, and now it seems, Rust. EDIT: Just because people may not know this: A relevant quote by Alan Perlis: "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy." This applies to type-level programming as it does any type of programming. EDIT#2: Also, look into Shen for a principled way to do this type of thing.
- dkarapetyan 10y ago
  Hence the ad-hoc part. I don't think people go into writing a type checker and type inferencer thinking they're gonna re-implement Prolog.
  - PeCaN 10y ago
    OTOH, if you're a Prolog programmer and you write a type checker, you rather quickly realize what's going on ;-)
mamcx 10y ago
Will have prolog make easier to implement the type system in a language? ie: I have base language (F#, for example) and wanna implement a new one, I do the type system on F#. If instead I add to the mix prolog, (or a prolog interpreter?) this will help a lot, or not worth the effort?
- pjmlp 10y ago
  I guess one way would be to use one of the mini kanren variants. http://minikanren.org/ http://minikanren.org/ There is also a F# implementation, https://github.com/palladin/logic https://github.com/palladin/logic
tatterdemalion 10y ago
In the near future, Rust's trait system literally will be a logic language similar to Prolog that runs at compile time. We walk the AST and generate statements to prove. This is expected to be easier to reason about, to be easier to extend, and to have shorter compile times - for essentially the reason you cite. Its even given us some (as yet unexplored) ideas for new extensions.
- deegles 10y ago
  Serious question... should I spend time in 2017 on Prolog? It seems like another case of "everything old is new again"...
  - pjmlp 10y ago
    Yes, you surely should, even if it is just wasting a few hours over a few weekends. Getting to grasp logic programming would improve your skills, even if you never use Prolog again. Use SWI-Prolog, one of the best free implementations out there. http://www.swi-prolog.org/ http://www.swi-prolog.org/
  - qznc 10y ago
    Yes, for the concepts. Just like it helps to know relational databases, even if you always use an ORM in practice. It is debatable if Datalog is enough or if cuts et al are worthwhile.
    - fauigerzigerk 10y ago
      Not sure if ORMs are a good analogy here. ORMs are a leaky and misleading abstraction on top of an actual RDBMS.
      - charlieflowers 10y ago
        The GP seems to be thinking in the opposite direction. His analogy is that knowing an ORM but not SQL is like not knowing Prolog, and that adding knowledge of SQL to your ORM knowledge is like learning Prolog. So the argument is that it is a similar eye-opening transition from ignorance to awareness.
alehander42 10y ago
I noticed that once and I even implemented a library which type checks Python with custom "type systems" written in Prolog, it was shocking how flexible is that, a bit like declarative grammars/parsing https://github.com/alehander42/hatlog https://github.com/alehander42/hatlog
joostdevries 10y ago
That's a result of the Curry Howard Lambek isomorphism. So I'm afraid it's not a new rule. :-)

by _qc3o 10y ago

badtuple 10y ago

Here's a great article about making the Prolog re-implementation in Rust's type system less ad-hoc and more awesome: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/ http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowe... The best days are when Niko posts about his work on Rust. Always interesting and they often exploit the power behind ideas like "It's basically Prolog" instead of apologizing for it. It's exciting and the kind of thinking that makes me remember why I fell in love with programming in the first place.

therein 10y ago

I read that with Bill Maher's voice in my head.

ruricolist 10y ago

Alternatively, you could just use Shen, which actually uses Prolog to implement its type system.

dkarapetyan 10y ago
Ya but for some reason Shen uses weird sequent calculus syntax. I'd much rather write Prolog rules than sequents.
throwaway7645 10y ago
Is the license for Shen still odd? I know Tarver doesn't believe in free software.
- mcbits 10y ago
  There is this page suggesting it's mostly BSD, but the License link is a 404: http://shenlanguage.org/ethics.html http://shenlanguage.org/ethics.html

lomnakkus 10y ago

If only. Prolog is actually reasonably pleasant to program in. Accidentally Turing Complete type systems are usually not all that pleasant in practice. Examples: C++ Templates, and now it seems, Rust. EDIT: Just because people may not know this: A relevant quote by Alan Perlis: "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy." This applies to type-level programming as it does any type of programming. EDIT#2: Also, look into Shen for a principled way to do this type of thing.

dkarapetyan 10y ago
Hence the ad-hoc part. I don't think people go into writing a type checker and type inferencer thinking they're gonna re-implement Prolog.
- PeCaN 10y ago
  OTOH, if you're a Prolog programmer and you write a type checker, you rather quickly realize what's going on ;-)

mamcx 10y ago

Will have prolog make easier to implement the type system in a language? ie: I have base language (F#, for example) and wanna implement a new one, I do the type system on F#. If instead I add to the mix prolog, (or a prolog interpreter?) this will help a lot, or not worth the effort?

pjmlp 10y ago
I guess one way would be to use one of the mini kanren variants. http://minikanren.org/ http://minikanren.org/ There is also a F# implementation, https://github.com/palladin/logic https://github.com/palladin/logic

tatterdemalion 10y ago

In the near future, Rust's trait system literally will be a logic language similar to Prolog that runs at compile time. We walk the AST and generate statements to prove. This is expected to be easier to reason about, to be easier to extend, and to have shorter compile times - for essentially the reason you cite. Its even given us some (as yet unexplored) ideas for new extensions.

deegles 10y ago
Serious question... should I spend time in 2017 on Prolog? It seems like another case of "everything old is new again"...
- pjmlp 10y ago
  Yes, you surely should, even if it is just wasting a few hours over a few weekends. Getting to grasp logic programming would improve your skills, even if you never use Prolog again. Use SWI-Prolog, one of the best free implementations out there. http://www.swi-prolog.org/ http://www.swi-prolog.org/
- qznc 10y ago
  Yes, for the concepts. Just like it helps to know relational databases, even if you always use an ORM in practice. It is debatable if Datalog is enough or if cuts et al are worthwhile.
  - fauigerzigerk 10y ago
    Not sure if ORMs are a good analogy here. ORMs are a leaky and misleading abstraction on top of an actual RDBMS.
    - charlieflowers 10y ago
      The GP seems to be thinking in the opposite direction. His analogy is that knowing an ORM but not SQL is like not knowing Prolog, and that adding knowledge of SQL to your ORM knowledge is like learning Prolog. So the argument is that it is a similar eye-opening transition from ignorance to awareness.

alehander42 10y ago

I noticed that once and I even implemented a library which type checks Python with custom "type systems" written in Prolog, it was shocking how flexible is that, a bit like declarative grammars/parsing https://github.com/alehander42/hatlog https://github.com/alehander42/hatlog

joostdevries 10y ago

That's a result of the Curry Howard Lambek isomorphism. So I'm afraid it's not a new rule. :-)