On 12 Jun 2015 10:17, "Matt Oliveri" <atma...@gmail.com> 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. Keean.
_______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
