On Fri, Jun 12, 2015 at 4:29 AM, Keean Schupke <[email protected]> wrote: > On 12 Jun 2015 09:15, "Matt Oliveri" <[email protected]> wrote: >> To possibly help reach an understanding regarding refinement types, I >> should probably point out here that refinement types are ideal when >> you're using types _only_ for static guarantees, like we are here. One >> should not expect refinement types to help with optimization; they're >> _too_ expressive. You'd have no idea what to do with the information >> refinements can provide in general. On the other hand, you never have >> to worry about refinement types hurting performance either, because >> you implement the unrefined type system; the refinements just get >> erased. > > What language has refinement types that I am going to implement my compiler > in? I guess I am thinking of generic techniques, rather than focusing on a > specific implementation language.
Right now? There is none, I don't think. Too bad. I never meant to imply that refinement types of the sort I want are ready to use. If we were only arguing about how to write programs in existing languages, I wouldn't be arguing for refinement types. >> This is why, Keean, it seems so strange to me to try to use type >> classes for refinements. Type classes definitely impact how code gets >> implemented. At least in Haskell. Refinements definitely do not. At >> least if you mean the same thing as me by "refinements". > > Type classes don't need to define any runtime code, and most of the > type-level functions implemented using type-classes in the HList paper > simply have the value 'undefined'. > > For example type level addition of Peano numbers: > > data Z > data S x > > class Add x y z | x, y -> z where > add :: x -> y -> z > > instance Add x Z x where > add _ _ = undefined > > instance Add x y z => Add x (S y) (S z) where > add _ _ = undefined Well I said it seems strange, not impossible. 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? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
