On 14 Jun 2015 7:47 am, "Matt Oliveri" <atma...@gmail.com> wrote:
> type(nat,z).
> type(nat,s(N)) :- type(nat,N).
Yes, that looks reasonable, although in implementation I will use an
infinite integer library to encode nats.
> Can you lift function types?
Well primitives have to exist on both levels. Probably only pure functions.
I think the answer is you can, but there are diminishing returns in terms
of complexity of implementation vs usefulness to the user. The question is
where to draw the line. I would like to keep unification decidable, and
there is a decidable subset of higher order stuff. Probably what can easily
be rewritten as first order is a good starting point.
> > So the predicate would be:
> >
> > has_two(X) :-
> > type(X, Y),
> > type(X, Z),
> > dif(Y, Z).
> >
> > Used as in:
> >
> > test :: has_two a => a -> a
>
> OK, this looks pretty close. The remaining problem is that the "dif"
> you defined in Haskell had the wrong meaning. ("Not known to be
> equal", rather than "known to be unequal".) Can you define a better
> dif in your new system?
Yes, but what definition is interesting.
> More generally, I'm concerned about the traditional reliance on the
> closed world assumption in logic programming. It should be possible to
> reason about programs modularly (that is, leaving things about other
> parts of the program unknown), but the closed world assumption seems
> to make bad things happen if you don't actually have all the facts
> when you run the proof search.
Yes, this is exactly what I am interested in right now. I've got something
to do now, but Ill follow up with some details later.
Keean.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
