has_two :: dif a b => (a, b)
has_two x y = (x, y)
Keean.
On 13 Jun 2015 12:14 pm, "Matt Oliveri" <atma...@gmail.com> wrote:
> 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 <atma...@gmail.com> wrote:
> > On Fri, Jun 12, 2015 at 7:30 AM, Keean Schupke <ke...@fry-it.com> wrote:
> >> On 12 Jun 2015 12:12, "Matt Oliveri" <atma...@gmail.com> 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
> bitc-dev@coyotos.org
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
