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. > 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 Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
