On Fri, Jun 12, 2015 at 7:30 AM, Keean Schupke <[email protected]> wrote:
> On 12 Jun 2015 12:12, "Matt Oliveri" <[email protected]> wrote:
>> I understand this. Remember we talked quite a bit about how you want
>> to use a stack of logic programming languages where each implements
>> the type system of the layer below. Or something like that. (And this
>> isn't type universes! You must not forget! ;) ) (The bottom layer
>> would be something like Haskell, I assume. But at any rate it would
>> not be another logic language.) So I have a rough idea of what you're
>> doing, I think, but practically do idea why you're doing it. Why the
>> fascination with type classes instead of real predicates?
>
> I am not sure there is a difference?
But are you sure there's _not_ a difference? :)
So what type classes seem useful for is:
1) Reasoning about the syntactic representations of types, by
imitating logic programming.
2) Asking for certain structure (the type class methods) on types.
(1) doesn't consider the meaning of types. That is, what elements they
have. (2) does, but it seems unable to say much about those elements.
Here's an example of a predicate on a type which is satisfied by all
types with at least two elements:
Definition HasTwo T := exists x y:T,x <> y.
("exists" is the existential quantifier. "<>" is "not equal to".)
I don't see how you'd express this as a type class, since it isn't
covered by (1) or (2).
Note that the "not equal" bit is not optional, because having "two"
elements which are the same doesn't count. For example,
class HasTwoSorta T where
x :: T
y :: T
is wrong. We can produce an instance for unit, which has only one
element, by taking both x and y to be ().
>> Logic programming instead of a real logic?
>
> I am not sure what you mean here? What is unreal about it? Firstly it is not
> Prolog, but has sound unification, a complete search strategy and I am
> working complete inference using negation elimination.
Algorithmic issues like unification, proof search, negation
elimination are not what I'm worried about. (Well actually, I'm kind
of worried about negation elimination.) I'm worried that the logic's
semantics are not rich. I don't know very much about it, but my
impression is that the semantics of logic programming is still
basically restricted to predicates on syntax trees.
It could be worse. ACL2's semantics are about equally restricted. But
for verifying big programs, you're going to miss the other goodies
that can be found in "mathematics-grade" logics. For example, real
predicates on types are nice. And they are a prerequisite for flexible
refinement typing.
> Secondly the language
> is a sub-structural logic, in which you can construct other logics from
> axioms.
Can the axiomatized logics be used to reason about programs? How would
soundness be ensured?
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
