On Fri, Jun 12, 2015 at 5:53 AM, Keean Schupke <[email protected]> wrote: > On 12 Jun 2015 10:17, "Matt Oliveri" <[email protected]> wrote: >> Note that "add" not being defined is not enough to guarantee that the >> Add type class will not affect the implementation of value-level >> functions that depend on an Add instance. Yes I know no-one will call >> add. The mere fact that the Add type class is involved allows an >> implementation to (foolishly) specialize based on it, or pass an Add >> dictionary at runtime. It requires extra implementation effort to >> recognize cases where type classes do not indicate a need for >> type-based dispatch. >> >> And even if it turns out that a type class encoding of refinements >> doesn't affect runtime. This still doesn't come anywhere close to >> establishing that the encodable refinements are expressive enough. >> >> Why, Keean? Why does it have to be type classes? What is so worthy >> about type classes that all things in type systems must be shoehorned >> into them? > > Type classes simply express constraints on types. Compare the definition of > the add type class with the following Prolog: > > add(X, z, X). > add(X, s(Y), s(Z)) :- add(X, Y, Z). > > So you can define any logical predicate on types, and I am just borrowing > Haskell's notation for expressing this as type classes.
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? Logic programming instead of a real logic? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
