Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!cs.ed.ac.uk!jha
From: jha@cs.ed.ac.uk (Jamie Andrews)
Newsgroups: comp.lang.prolog
Subject: Re:  general data structures are [not] impossible
Message-ID: <6896@skye.cs.ed.ac.uk>
Date: 27 Feb 91 21:05:45 GMT
References: <6406@skye.cs.ed.ac.uk> <9732@uwm.edu>
Sender: nnews@cs.ed.ac.uk
Reply-To: jha@lfcs.ed.ac.uk (Jamie Andrews)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 45

In article <9732@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes:
>Predicates ARE records only in disguise...
>PASCAL:
>type Complex = record RE, IM: real end;
>PROLOG:
>complex(RE, IM) :- real(RE), real(IM).

     The point of some of the previous postings is that the
lookup for this kind of thing may be too expensive -- ie. O(n)
where n is the size of the program, if we're implementing it
naively, rather than a small constant in the case of pointers.

     Even if we had efficient lookup for special predicates used
in this way, there would still be the problem of building such
data structures at runtime (with assert and retract?).  I'm
afraid the ideal is still the use of looping data structures as
actual data objects (that can be passed around as parameters).
Some logical description of the types may still be possible, but
that's different than using the existing predicate mechanisms to
do looping data objects.

>Also, if you consult the lambda calculus and functional programming literature,
>you'll find out about results concerning the correspondence (isomorphism)
>between types and propositions which underlies this observation
>(records <-> AND, unions/variants <-> OR, functions <-> IMPLICATION, etc.)

     Hmm.  This "Curry-Howard" isomorphism is really about
treating formulae (A, B, C) as "types", the data objects of
types A, B, C being formal descriptions of the proofs of A, B,
C.  The fact that these formal descriptions of proofs take the
form of records, unions etc. is incidental -- no general data
structures are necessarily being encoded.

     Curry-Howard does make proofs of type membership and proofs
of formulae into the same thing.  But in a logic programming
setting this reduces to using a type-theoretic (say, ML-style)
type discipline for data object types.  This is the approach
advocated by people like Frank Pfenning.  From your remarks
about flexibility, I think what you're talking about is more
like Uday Reddy et al.'s approach of using
predicate-definition-like constructs to describe types.

--Jamie.
  jha@cs.ed.ac.uk
"'He acts crazy, I guess.  We all act crazy.  I guess God acts crazy.'  Etc."