DEV Community

Discussion on: The Curry-Howard Correspondence in C#: Part 2

View post
Collapse
 
johnkazer profile image
John Kazer •

What's the relationship of this concept to Prolog? It's been too long since I used the language but it seems to be conceptually related...
This example Prolog repl seems an nice way to play with the idea. For example, given the propositions

loves(vincent, mia).
loves(marcellus, mia).
loves(pumpkin, honey_bunny).
loves(honey_bunny, pumpkin).

jealous(X, Y) :-
    loves(X, Z),
    loves(Y, Z).
Enter fullscreen mode Exit fullscreen mode

type

loves(X, mia).
Enter fullscreen mode Exit fullscreen mode

in the query terminal and hit 'run'!

Collapse
 
shimmer profile image
Brian Berns •

Good question. Prolog is a very cool language, but is based on different logical principles. The Curry-Howard correspondence actually leads to theorem-proving languages like Coq, Agda, Idris, and F* that support "dependent types". I might try to blog a little about this in the future.

In the meantime, here's a good Stack Overflow question that goes into the differences between Prolog and C-H correspondence in more detail.