## Dependent Types in Prolog

### Wednesday, 7th May, 2014

or, “Had we but world enough, and time …”

**** intro**

I’ve been occasionally looking into programming languages with dependent types, when a recent tweet gave me pause:

So.

I got interested in dependent types because SO TOLD ME TO^W^W^W^W they seemed necessary to encode some constraints on types for some toy projects I was thinking of, namely:

- for a Bayesian network: represent probabilities (positive floating point number less than or equal to 1.0) and discrete probability distributions (a {T, Probability} mapping where the sum of probabilities = 1.0);
- for fast Fourier transformation: respresent a list whose length must be a power of 2.

Naively, I thought I might be able to do this kind of thing in Haskell. I don’t like the cult hype around Idris. I thought I might try it with ATS, which I like the look of a lot, but it’s proving slow getting into.

**** prolog**

In the meantime, here are the types represented in Prolog:

% some "dependent" types %%%% X is a power of 2 pow2(2). pow2(X):- integer(X), Y is X / 2, pow2(Y). %%%% X is a list whose length is a power of 2 lp2([]). lp2(X):- is_list(X), length(X, L), pow2(L). %%%% X is a probability prob(X):- float(X), X >= 0, X =< 1. %%%% X is a discrete probability distribution dpd(X):- tuplist(X), seconds(X,Y), maplist(prob, Y), sum_list(Y, 1.0). %%%% helpers seconds([], []). seconds([[_, Y] | Z], [Y | Z2]):- seconds(Z, Z2). tuplist([]). tuplist([[_X, _Y] | Z]):- tuplist(Z).

**** next**

So.

I might yet try this with ATS.

On the other hand, I might try it with Mercury, which seems to be (among other things perhaps) a typed Prolog.

**** p.s.**

In case the above is a bit downbeat on ATS: I do think ATS is a very interesting language. If any reader can give a quick sketch of one of the simpler types above in ATS, I am definitely up for having a go at the others.

Friday, 9th May, 2014 at 9:30 pm

Hello,

Thanks for posting this, and thanks for being excited about dependent types, however I feel compelled to suggest that your example doesn’t actually contain dependent types. Instead, I think what you have produced is more akin to runtime contracts. Constraints that are enforced when the program is executed, not inferred prior to runtime.

That being said, it’s easy to confuse the two. I’ve certainly done it before. Dependent types are similar to contracts in the sense that we often see them guarding functions from being called with incorrect inputs–but instead of occurring at runtime DT guards are checked prior to the program even being executed.

For a simple idea of how this is useful, think of a division function that should throw an error whenever a zero is given as a divisor. What happens? The standard answer is that it returns ‘infinity’, but this is unsatisfying on a number of levels. Among them is that it can’t be computed. We could probably settle for catching this error at runtime, but DT can do better. With existing compilers, a number can’t be determined before a program is run. On the 100th call to the function it could have a zero for its value and the compiler would miss it. DT, on the other hand, inspects all the possible interpretations of the function and is able to make guarantees about which values are actually possible. If a zero cannot be given to a function, then there is no need to worry about that possibility. Languages like Idris and ATS can make these undesirable situations impossible. (e.g. https://gist.github.com/gbluma/dd6dea90141fa21845ea)

As for the “cult hype around Idris,”… Sure, I can see why it might seem that way. We’re excited about dependent types for the real benefit they will add, and Idris is the most practical means for exploring that right now. DT is a fundamentally new thing that most people have never seen. Overall the theory is also ahead of the implementation, so most of us read a lot waiting for more mature implementations. Those of us aware of DT know that it will have a significant impact on software practices where security, reliability, and maintainability are important.

Anyway, just thought I’d share. Keep exploring. :)

—

Garrett

Saturday, 10th May, 2014 at 10:20 am

Dear Garrett

Thank you for your comment.

Perhaps I should have been clearer. The predicates are type-test predicates just like the ones found in prolog. They would be used by a type-checker to verify the types in a third prolog program. As far as I can see, this checking could be done during run-time or at compile-time of that third program. The choice of run-time or compile-time type checking is pragmatic surely, or is there more to it?

Type checkers in prolog seem to be “roll-your-own” (e.g., a, b, c) so I thought I would try and avoid that and see if I could implement these types in Mercury.

As for Idris: if you can demonstrate how to implement the probability type above, I’ll put Idris back on the shortlist. At CodeMesh last year, Edwin Brady gave me the impression it was not plausible.

Best wishes

Ivan