On Sun, Jun 14, 2015 at 2:04 AM, Keean Schupke <[email protected]> wrote:
> On 14 Jun 2015 6:48 am, "Matt Oliveri" <[email protected]> wrote:
>>
>> It was a contrived example, I don't know any use to program
>> verification off the top of my head. However it's meaning, that I gave
>> in English, should be intuitively clear.
>>
>> (HasTwo T) should be true, where T is a type, if and only if T has at
>> least two elements.
>> For example, (HasTwo bool) is true. (HasTwo nat) is true. (HasTwo
>> unit) is false. (HasTwo T), where T is an abstract type, is unknown.
>
> Well I can't think of an easy way to do it in Haskell.
>
> Type definitions get lifted like this:
>
> type(bool, true).
> type(bool, false).
So you'd lift nat like this?
type(nat,z).
type(nat,s(N)) :- type(nat,N).
Can you lift function types?
> 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?
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.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
