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:


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

    Y is X / 2,

%%%% X is a list whose length is a power of 2

    length(X, L),

%%%% X is a probability

    X >= 0,
    X =< 1.

%%%% X is a discrete probability distribution

    maplist(prob, Y),
    sum_list(Y, 1.0).

%%%% helpers

seconds([], []).
seconds([[_, Y] | Z], [Y | Z2]):-
    seconds(Z, Z2).

tuplist([[_X, _Y] | Z]):-

** next


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.

Building and installing ATS on FreeBSD

Wednesday, 30th April, 2014

ATS is a statically typed functional (eager) programming language with dependent types and linear types. It “can be as efficient as C/C++ both time-wise and memory-wise”.

Building and installing on FreeBSD is mostly straightforwardly following the documentation, but three things tripped me up:

GNU make vs BSD make

The Makefiles assume GNU make and won’t run with BSD make. However, on FreeBSD, “make” is BSD make, and GNU make is “gmake”. The way the Makefiles are written (e.g., make is called explicitly from within the Makefiles) seemed to rule out just aliasing gmake as make, so I (as root) hid (BSD) make and symlinked “make” to gmake.

which compiler

By default the Makefiles compile with gcc, although there is an option to compile with clang. My FreeBSD set up had both, with clang as the default compiler (at cc). However, although gcc was installed, it was at “gcc47” and there was no symlink from “gcc”. I added the symlink.


In the install_files sections of the top-level Makefile, the install commands have a space between the -m flag and the actual mode, e.g.:

    105  install_files_1: bin/patscc ; \
    106    $(INSTALL) -T -m 755 $< $(PATSLIBHOME2)/bin/patscc && echo $<

This tripped up install, which reads that 755 as a separate argument. This is fixed by removing the space, i.e.:

    105  install_files_1: bin/patscc ; \
    106    $(INSTALL) -T -m755 $< $(PATSLIBHOME2)/bin/patscc && echo $<

There are five points which need to be changed.

(n.b.: the Makefile may have been updated by the time you read this.)


With all that done, and a “Hello world!” program compiled and run, I am ready to adventure into dependent and linear types!