Hacker News new | ask | show | jobs
by aweinstock 2026 days ago
Section 5.13 advises building a custom type-and-mode checkers (per project, seemingly).

Section 4.1 defines a specific type-and-mode system in enough detail that it seems machine-checkable (potentially with the declarations as-is, with suitable declarations of unary `+` and `-` via `op/3` for modes).

It feels like an omission that the paper doesn't recommend or even mention the existence of an implementation-agnostic, project-agnostic type-and-mode checker.

Has one been developed since the paper was published, or is this not as useful as it would seem/not done for some other reason?
1 comments
YeGoblynQueenne 2025 days ago
There are a few community libraries, for example see the Swi-Prolog packages typedef [1] and typecheck [2] (the latter implementing Hindley-Milner). Unfortunately there isn't anything like an accepted standard (although the package typedef is very popular).

My experience is that type- and mode-checking in Prolog programs tends to be ad-hoc and simplistic, for example it's common to test whether an argument is ground or not and therefore enforce a certain mode (or sets of modes):

  % p(+X,-Y)
  % 
  p(X,Y):- 
    ground(X)
    ,var(Y)
    ,...
For slightly more complex type-checking the Prolog ISO standard provides predicates like integer/1, atom/1, atomic/1 etc [1]. These don't make up a proper type system but they can go a long way towards catching common errors.

A subtler point is that Prolog programs tend to use unification to perform type-checking by pattern matching an argument to a (Prolog) term. For example (borrowed from a Prolog course I'm GTA'ing):

  max_heap(epsilon).
  max_heap(h(K-V, L, R)) :-
    \+ root_max(L, K),
    \+ root_max(R, K),
    max_heap(L),
    max_heap(R).

  root_max(h(Kr, _, _, _), K) :-
    Kr > K.
This will fail for any (at least partially ground) input to max_heap/1 that doesn't match the term h(K-V,L,R), here used to represent a binary heap, or the atom "epsilon", for the empty heap. The representation of a heap in this way is entirely up to the programmer but Prolog's built-in unification will essentially provide type-checking for free when a complex data structure like this is used.

_______________

[1] https://www.swi-prolog.org/pack/list?p=typedef

[2] https://www.swi-prolog.org/pack/list?p=type_check

[3] See: https://www.swi-prolog.org/pldoc/man?section=typetest for a swanky ASCII diagram.

link