Re: DCGs as algebraic types

On 10/11/2013, at 11:59 PM, Stassa Patsantzis wrote:
>> A list of terminals must be a *proper* list.
> 
> How about this?
> 
>     list --> [].
>     list --> [_H], list.

That's fine, that's a list of anything.
> 
> And: 
> 
>     list --> [].
>     list --> [H], { type([H], []) }, list.
> 
>     type --> [t] | [y] | [p] | [e].

That's a long-winded way to write

	list --> [].
	list --> [H], {member(H, [t,y,p,e])}, list.

>>> data List a = Nil | Cons a (List a)
> 
>> That corresponds to a plain predicate:
> 
>>     'List'(A, 'Nil').
>>     'List'(A, 'Cons'(H, T)) :-
>>         call(A, H),
>>         'List'(A, T).
>     
> That's very useful, thank you. Is this coming from some work you've already done
> on this sort of thing? Is it a common pattern that I should know from the (few) 
> sources I've read?

It's a pattern which was used heavily in the DEC-10 Prolog library
back in the early 80s, although that did things like

	is_list(*) :- !, fail.
	is_list([]).
	is_list([_|T]) :-
	    is_list(T).

in order to (a) recognise only terms whose (type-specific)
skeleton was instantiated and (b) not go into infinite loops.
(The *right* answer is a strong mode system like Mercury's.)

data T x1 ... xn
   = C1 a11 ... a1n1
   | ...
   | Ck ak1 ... aknk
=>

'T'(X1, ..., Xn, 'C1'(A11,...,A1n1)) :-
    a11'(A11),
    ...
    a1n1'(A1n1).
...
'T'(X1, ..., Xn, 'Ck'(Ak1,...,Aknk)) :-
    ak1'(Ak1),
    ...,
    aknk'(Aknk).

where if aij is xm, aij'(Aij) is call(Xm, Aij)
and if aij is (Tm xm1 ...), aij'(Aij) is 'Tm'(Xm1,...,Aij),
and so on.

For GADTs, I'll just take an example:

data T a where
    D1 :: Int    -> T String
    D2 ::           T Bool
    D3 :: a -> a -> T [a]

turns into

'T'('String', 'D1'(I))   :- 'Int'(I).
'T'('Bool',   'D2')).
'T'(list(A),  'D3'(X,Y)) :- call(A, X), call(A, Y).

> I think the above is pretty similar to my example, especially the revised one. 
> "call(A,H)" is very much like "type([H], [])" I think, where A is type//0. 

It's not that similar.  call(A, H) says "given that A is a term naming a
type, which is represented by a system of clauses, check that data term
H belongs to that type."  type([H], []) is a long-winded way of saying
that H must be one of a *specific* set of values.  The lists here serve
no purpose, and the "type parameter" A is missing.

The argument order here is "type terms, data term" so that we can
do things like call('T3'(list(list('Int'))), X).
> 
> 
>> The analogy between data types and grammars has been known
>> longer than Prolog has existed; it's one of the key ideas
>> behind Jackson Structured Programming.
> 
> OK, thanks, that's also very useful. Also a bit embarassing I had never seen 
> this before but it's good to know I'm on solid ground so far. 

http://en.wikipedia.org/wiki/Jackson_structured_programming
"JSP uses semi-formal steps to capture the existing structure of
a program's inputs and outputs in the structure of the program itself.

The intent is to create programs which are easy to modify over
their lifetime.  Jackson's major insight was that requirement
changes are usually minor tweaks to the existing structures.
For a program constructed using JSP, the inputs, the outputs,
and the internal structures of the program all match, so small
changes to the inputs and outputs should translate into small
changes to the program."

Leon Sterling also made much of the fact that the structure of
a Prolog predicate tends to resemble the structure (or perhaps
the grammar) of the (principal) data type it is working on;
you can see the data-type recogniser as a template for code
that works on such data.  So we'd have

p('D1'(I), Ans) :-
    do something with I and Ans.
p('D2', Ans) :-
    do something with Ans.
p('D3'(X, Y), Ans) :-
    do something with X Y and Ans.

Since the data type isn't recursive, neither is the predicate.
I _think_ this is in The Art of Prolog by Sterling and Shapiro,
and I _think_ it's in "Patterns for Prolog Programming" by
Leon and "Stepwise Enhancement and Higher Order Programming
in Prolog" by Lee Naish and Leon Sterling has something about it.

> 
> OK, lots more thought needs to go into this. I think maybe one reason why DCG's 
> appeal to me is because they lend an air of the imperative, or the functional, 
> to Prolog.

Hmm.  Well, *kind* of.  It's more like the idea of using monadic
parser combinators in Haskell.  Yes, Haskell *does* use the IO
monad for I/O, and yes, Haskell *does* use monads for mutable
arrays, but no, monadic parser combinators *aren't* imperative
in any interesting sense.

(There is a fairly clear link between DCGs and parser combinators...)

DCGs are an extremely useful notation for *constructing* lists.
One of the passes in the Quintus Prolog compiler used a DCG to
construct the list of instructions.  Thinking of them as
imperative or functional will stop you thinking of them for
this use case.

Another idea is to think of *traces* of a program (see for example
Hoare's "Communicating Sequential Processes" book for a concurrent
language defined via traces) and to describe the traces using DCGs,
possibly extended with some of the extra operations in Hoare's book
(which can be found free on-line).  Maybe you can use partial
execution to eliminate the DCGs and leave behind code that generates
the desired traces (that is, behaves as described by the traces)
directly.

>  So, if we see 
> DCG's as a way to map inputs to outputs, maybe instead of fiddling about with 
> messy mode declarations we can write grammar rules to point out to the compiler 
> the input-to-output relations in our programs?

I don't see how to do that, but it's not obviously crazy,
so maybe you have a new idea that's worth exploring.
> 
>> But yes, there is a reason not to use DCGs for type checking: most
>> data types are not lists.
> 
> Well, yes, but. Grammars aren't lists either.

No, but they *describe* lists.

> We use lists as a convenient data structure to represent a grammar.

Where?  In Prolog we (often) represent a grammar as a DCG,
and a DCG is not a list.

Oh, there are plenty of other kinds of grammar.
There are 2D grammars (which have been used for image recognition);
there are tree grammars (look up Tree-Adjoining Grammar); there are
graph grammars; you name a structure and there's probably some kind
of grammar for it.

Perhaps the most important thing about DCGs is the idea
that you can define your *own* kind of grammar and translate it
to plain Prolog.  There's an entire book about various kinds of
grammar in Prolog, but there's a stack of boxes in front of my
copy (:-(.

> So, shifting the goalposts a bit, is it 
> convenient to represent a type as a grammar represented by lists?

I don't know.  I don't even know how you propose to represent a
grammar as lists.  Try it and find out.

The one time I tried to discourage someone with an original idea,
it became a major subarea of CS with multiple journals and conferences
twelve years later.  I'm not going to do that again!

(Who would have thought that homotopy had anything to do with types?
But it has: homotopytypetheory.org/‎ )

_______________________________________________
SWI-Prolog mailing list
[email protected]
https://lists.iai.uni-bonn.de/mailman/listinfo.cgi/swi-prolog