3 ms·

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 th

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?

YeGoblynQueenne 6y 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 https://www.swi-prolog.org/pack/list?p=typedef [2] https://www.swi-prolog.org/pack/list?p=type_check https://www.swi-prolog.org/pack/list?p=type_check [3] See: https://www.swi-prolog.org/pldoc/man?section=typetest https://www.swi-prolog.org/pldoc/man?section=typetest for a swanky ASCII diagram.

YeGoblynQueenne 6y 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 https://www.swi-prolog.org/pack/list?p=typedef [2] https://www.swi-prolog.org/pack/list?p=type_check https://www.swi-prolog.org/pack/list?p=type_check [3] See: https://www.swi-prolog.org/pldoc/man?section=typetest https://www.swi-prolog.org/pldoc/man?section=typetest for a swanky ASCII diagram.