This thread is to discuss the use of type classes to simulate predicates. It picks up a loose end from the "LR vs Static Typing" thread, but it's really more like a successor of the "Refinement types" thread.
I'm still in the middle of a disagreement with Keean about whether type classes are an adequate substitute for refinement types. To me the answer seems to be no, without a ludicrous extension to the instance resolution rules. But Keean still seems to believe the answer is yes. I think the key question is whether type classes, used as predicates, are expressive enough to be the predicates that act as type refinements. On Fri, Jun 12, 2015 at 9:09 AM, Matt Oliveri <[email protected]> wrote: > 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: >>> 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. I assume (2) is the main/intended use case of type classes, but Keean seems to be basing his refinements on the ability to do (1). (Though it's technically irrelevant, this already makes it seem like a hack to me.) > (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 (). Although I'm still curious whether HasTwo can be defined as a type class, it isn't technically necessary in order to do refinement types, since the predicates for refinement types are predicates on values. Keean is encoding values as types (another hack?), because type classes are only predicates on types. But this only means that type classes need to be expressive-enough predicates on encoded values. > 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. I should probably start by finding out if Keean's approach can really match ACL2. The nicest thing ACL2 doesn't have is probably first-class functions. > And [predicates on types] are a prerequisite for flexible > refinement typing. That was wrong. I had confused myself. That's probably how I chose HasTwo in the first place. But type predicates would still probably come in handy. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
