If you really want, I can define dif in Haskell:
class Dif x y where
dif :: x -> y -> ()
instance Undefined(x) => Dif x x where
dif _ _ = undefined
instance Dif x y where
dif _ _ = undefined
Where "Undefined" is any undefined type class. Due to Haskell's matching
rules for overlapping instances the closet match wins, so dif succeeds if
the types are different, but fails due to committed choice semantics when
it cannot find an instance of Undefined for x.
Keean.
On 13 Jun 2015 12:25 pm, "Keean Schupke" <ke...@fry-it.com> wrote:
> 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
