Fw: DCGs as algebraic types

Hi Richard, 


Please excuse the late reply; long week at work this one, very few brain cycles
left at the end of each day. 

> A list of terminals must be a *proper* list.

How about this?

    list --> [].
    list --> [_H], list.

And: 

    list --> [].
    list --> [H], { type([H], []) }, list.

    type --> [t] | [y] | [p] | [e].

I'm trying to avoid using context-sensitive rules, though not for any particular
reason other than keeping it all as neat looking as possible. 
    
>> 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? 

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. 

listing/1 my example, I get: 

    list(A, A).
    list([A|B], D) :-
        type([A], []),
        C=B,
        list(C, D).

- where arguments are back-to-front a bit but it generally looks the same to me.

Mistakes?
 Misunderstandings?


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

Let's change that. 

> What does Jackson's idea of a "structure clash" have to teach us about
> writing Prolog code?

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. I mean the way everything is described in terms of inputs and outputs 
and you can replace non-terminals with their outputs in a rule body, much like 
in the body of a function... er, which is exactly what happens to a function 
body when its parse tree is built during
 compilation. Hum hum. Well...

No, let's go back to what you said. In Prolog we learn to explicitly _not_ think 
of programs as sets of inputs and outputs, because predicates aren't functions; 
and we learn (eventually) that DCG's are simply an interface to ordinary Prolog 
predicates, syntactic sugar to bitter-tasting difference lists. 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? Even more, we can declare the 
types of data in our program, using that same grammar, in fact the same grammar 
that forms the program (though that's probably not to everyone's taste). Then 
verifying the types of data in our program would be a simple matter of running 
the program, which would naturally fail if there was some type error. Inputs of 
the wrong type
 would be found to be grammatically incorrect for the program and 
cause the whole thing to fail. I'm overlooking for now how with a DCG you can 
always treat your inputs as outputs. C.A.R. Hoare would have a giraffe :)  

Btw, I always thought this 'imperative air' is probably the wrong reason to find 
DCG notation attractive, but maybe it's not that wrong after all. 

Also, this time I know that all of the above is definitely nothing new- that's 
just how declarative programming is supposed to work. And I guess it's not quite 
what you were driving at with your questions, but then I'm sure you expected
that :)


> 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. We use lists as a convenient data
structure to represent a grammar. So, shifting the goalposts a bit, is it 
convenient to represent a
 type as a grammar represented by lists?

Another little observation (sorry, this is growing too long). A predicate
is already a type basically, each clause one of its members. Well, that's not 
anything new either, Curry-Howard and programs-as-proofs and all that.  

OK I'll stop here. Too much babbling for a Sunday morning :)

Thanks for the input Richard and sorry for the torrential output. My day job 
bores me so much these days :)

Cheers! 
Stassa    



On Saturday, 2 November 2013, 2:01, "[email protected]" <[email protected]> wrote:
 
> Hi list,
>
> When I look at a grammar rule like the following:
>
> list --> [].
> list --> [H|T], { list(T,[]) }.

That second rule is exceptionally strange.  I am away from home
and do not have ready access to the draft DCG specification for
the standard, but it's not even clear to me that it is legal.
A list of terminals must be a *proper* list.

>
> - I can't help but think that it looks a lot like an algebraic data type.
> Say
> for instance, the following example from wikipedia:
>
> 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).

The general construction should be fairly obvious.
There is a predicate for each type constructor, having
one data argument (the last), and an argument for each
type parameter.  There is a clause for each data constructor.
This approach is not limited to ADTs but can handle GADts as
well.

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.


> So does
 that all sound too naive? Or did I just reinvent someone's wheel?
> Is
> there any good reason why not to use DCG's to do type checking like above?

You _have_ reinvented a wheel, but it's a good firm properly circular
wheel with a lot of mileage left.  There is bound to be some more
insight to be won from it.  As there are interesting classes of
grammars, are there interesting classes of types?  What if you think
about Tree and/or Graph grammars instead of sequence grammars?  What
does Jackson's idea of a "structure clash" have to teach us about
writing Prolog code?

But yes, there is a reason not to use DCGs for type checking: most
data types are not lists.
-------------- next part --------------
HTML attachment scrubbed and removed