## 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.

### 2 Responses to “Dependent Types in Prolog”

1. gbluma Says:

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

• llaisdy Says:

Dear Garrett