This is pure speculation, inspired in part by Brent Yorgey's blog post[1] from a few weeks ago. I'm wondering if it might be possible, in theory, to have both open and closed variants for each of value-level functions, type functions, and classes, in a fairly analogous way. (Maybe you could even have open (G)ADTs, which you would then need open functions to match on; or maybe a closed one with a case for _ to ensure exhaustiveness.) In each case you'd have the closed variant requiring you to keep all the definitions in the same module, permitting overlap, and trying to match definitions in the order they're listed; whereas the open variant would let you have definitions across modules, would forbid overlap (or would require definitions to be equivalent where they overlap, as with type families), and would always select the uniquely matching definition. Open value-level functions with this scheme would be inherently partial, which is bad. (It's not a problem at the type level because you just get a compile error if nothing matches, but an exception at runtime isn't so nice.) As a solution, perhaps it might be possible to allow a limited form of overlap (or don't even call it overlap) for the open variants: a default "use this is if nothing else matches" definition (which would need to be in the same module as the original class / type family declaration, or whatever ends up being analogous for open value-level functions, maybe the type signature). That way you could use Maybe for open value-level functions and make the default Nothing, among other options. Overlap in type functions allegedly makes typechecking unsound; I don't know if that would also hold in this more limited case. This would definitely break the property where adding or removing an import can't change the behaviour of a program other than whether it compiles, which is considered very important by many [2], so maybe it's not a good solution. (Possibly you could add explicit import/export control for instances/other-open-things to alleviate this, in a way so that definitions for open thingies with default definitions (at least) would always have to imported explicitly, thereby acknowledging that it might change behaviour... or maybe that would be a bandaid too far, I dunno.) (I think this would also cover most (if not all?) of the use cases for OverlappingInstances, which permits overlap and selects the most specific instance in a more general fashion; but maybe that doesn't matter if the two are equally bad, I don't know. I'm not 100% clear on peoples' opinion of OverlappingInstances, but I as far as I know the problems are twofold: both import-unsafeness, and the matter of how you would actually define "most specific" in a way that's both rigorous and intuitive; this would remove at least the latter.) Anyway, thoughts? Is this all completely crazy and way out there? [1] http://byorgey.wordpress.com/2010/08/05/typed-type-level-programming-in-hask... [2] http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities -- Work is punishment for failing to procrastinate effectively.
Hi, The details of the issues involved in an open and closed facility for Haskell are way beyond my current understanding of the language. Nonetheless, I was wondering does this have anything to do with the expression problem? Pat 17/08/2010 14:48 Victor Nazarov asviraspossible@gmail.com wrote:
Finally tagless technique seems to solve expression problem using pretty basic Haskell:
-------------------------------------------------- module AddExp where class AddExp e where add :: e -> e -> e lit :: Int -> e
-- Type signature is required -- monomorphism restriction will act otherwise test :: AddExp e => e test = add (lit 6) (lit 2)
----------------------------------------------------- module MulExp where class MulExp e where mul :: e -> e -> e
-- Type signature is required -- monomorphism restriction will act otherwise test1 :: (AddExp e, MulExp e) => e test1 = mul test (lit 3)
----------------------------------------------------- module Evaluator
import AddExp where
newtype Eval = E { eval :: Int }
instance AddExp Eval where lit = E add (E a) (E b) = E (a + b)
----------------------------------------------------- module PrettyPrinter where
import AddExp import MulExp
newtype PrettyPrint = P { prettyPrint :: String }
instance AddExp (PrettyPrint) where lit n = show n add (P a) (P b) = concat [a, " + ", b]
instance MulExp (PrettyPrint) where mul (P a) (P b) = concat [a, " * ", b]
-- Victor Nazarov
Gábor Lehel wrote:
This is pure speculation, inspired in part by Brent Yorgey's blog post[1] from a few weeks ago.
I'm wondering if it might be possible, in theory, to have both open and closed variants for each of value-level functions, type functions, and classes, in a fairly analogous way. (Maybe you could even have open (G)ADTs, which you would then need open functions to match on; or maybe a closed one with a case for _ to ensure exhaustiveness.)
In each case you'd have the closed variant requiring you to keep all the definitions in the same module, permitting overlap, and trying to match definitions in the order they're listed; whereas the open variant would let you have definitions across modules, would forbid overlap (or would require definitions to be equivalent where they overlap, as with type families), and would always select the uniquely matching definition.
Open value-level functions with this scheme would be inherently partial, which is bad. (It's not a problem at the type level because you just get a compile error if nothing matches, but an exception at runtime isn't so nice.) As a solution, perhaps it might be possible to allow a limited form of overlap (or don't even call it overlap) for the open variants: a default "use this is if nothing else matches" definition (which would need to be in the same module as the original class / type family declaration, or whatever ends up being analogous for open value-level functions, maybe the type signature). That way you could use Maybe for open value-level functions and make the default Nothing, among other options. Overlap in type functions allegedly makes typechecking unsound; I don't know if that would also hold in this more limited case. This would definitely break the property where adding or removing an import can't change the behaviour of a program other than whether it compiles, which is considered very important by many [2], so maybe it's not a good solution. (Possibly you could add explicit import/export control for instances/other-open-things to alleviate this, in a way so that definitions for open thingies with default definitions (at least) would always have to imported explicitly, thereby acknowledging that it might change behaviour... or maybe that would be a bandaid too far, I dunno.)
(I think this would also cover most (if not all?) of the use cases for OverlappingInstances, which permits overlap and selects the most specific instance in a more general fashion; but maybe that doesn't matter if the two are equally bad, I don't know. I'm not 100% clear on peoples' opinion of OverlappingInstances, but I as far as I know the problems are twofold: both import-unsafeness, and the matter of how you would actually define "most specific" in a way that's both rigorous and intuitive; this would remove at least the latter.)
Anyway, thoughts? Is this all completely crazy and way out there?
[1] http://byorgey.wordpress.com/2010/08/05/typed-type-level-programming-in-hask... [2] http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
I'm not sure if they're within my own, either. The expression problem
did fleetingly cross my mind while thinking about this. Open ADTs +
open functions might be a very simple solution to it - that is, if
they make sense at all. I haven't thought it through thoroughly
though.*
Another thing I'm wondering about is that there's a fairly intuitive
correspondence between functions at the value level vs. functions at
the type level, and datatypes to classify the value level vs.
datakinds to classify the type level, but what corresponds to type
classes at the value level? There's also all kinds of weird
interactions like whether you could have an open function as the
implementation of a type class method.
* I think this might be some kind of personal record for density of
unique words matching /th[a-z]*ough[a-z]*/ in a single sentence.
2010/8/29 Patrick Browne
Hi, The details of the issues involved in an open and closed facility for Haskell are way beyond my current understanding of the language. Nonetheless, I was wondering does this have anything to do with the expression problem?
Pat
17/08/2010 14:48 Victor Nazarov asviraspossible@gmail.com wrote:
Finally tagless technique seems to solve expression problem using pretty basic Haskell:
-------------------------------------------------- module AddExp where class AddExp e where add :: e -> e -> e lit :: Int -> e
-- Type signature is required -- monomorphism restriction will act otherwise test :: AddExp e => e test = add (lit 6) (lit 2)
----------------------------------------------------- module MulExp where class MulExp e where mul :: e -> e -> e
-- Type signature is required -- monomorphism restriction will act otherwise test1 :: (AddExp e, MulExp e) => e test1 = mul test (lit 3)
----------------------------------------------------- module Evaluator
import AddExp where
newtype Eval = E { eval :: Int }
instance AddExp Eval where lit = E add (E a) (E b) = E (a + b)
----------------------------------------------------- module PrettyPrinter where
import AddExp import MulExp
newtype PrettyPrint = P { prettyPrint :: String }
instance AddExp (PrettyPrint) where lit n = show n add (P a) (P b) = concat [a, " + ", b]
instance MulExp (PrettyPrint) where mul (P a) (P b) = concat [a, " * ", b]
-- Victor Nazarov
Gábor Lehel wrote:
This is pure speculation, inspired in part by Brent Yorgey's blog post[1] from a few weeks ago.
I'm wondering if it might be possible, in theory, to have both open and closed variants for each of value-level functions, type functions, and classes, in a fairly analogous way. (Maybe you could even have open (G)ADTs, which you would then need open functions to match on; or maybe a closed one with a case for _ to ensure exhaustiveness.)
In each case you'd have the closed variant requiring you to keep all the definitions in the same module, permitting overlap, and trying to match definitions in the order they're listed; whereas the open variant would let you have definitions across modules, would forbid overlap (or would require definitions to be equivalent where they overlap, as with type families), and would always select the uniquely matching definition.
Open value-level functions with this scheme would be inherently partial, which is bad. (It's not a problem at the type level because you just get a compile error if nothing matches, but an exception at runtime isn't so nice.) As a solution, perhaps it might be possible to allow a limited form of overlap (or don't even call it overlap) for the open variants: a default "use this is if nothing else matches" definition (which would need to be in the same module as the original class / type family declaration, or whatever ends up being analogous for open value-level functions, maybe the type signature). That way you could use Maybe for open value-level functions and make the default Nothing, among other options. Overlap in type functions allegedly makes typechecking unsound; I don't know if that would also hold in this more limited case. This would definitely break the property where adding or removing an import can't change the behaviour of a program other than whether it compiles, which is considered very important by many [2], so maybe it's not a good solution. (Possibly you could add explicit import/export control for instances/other-open-things to alleviate this, in a way so that definitions for open thingies with default definitions (at least) would always have to imported explicitly, thereby acknowledging that it might change behaviour... or maybe that would be a bandaid too far, I dunno.)
(I think this would also cover most (if not all?) of the use cases for OverlappingInstances, which permits overlap and selects the most specific instance in a more general fashion; but maybe that doesn't matter if the two are equally bad, I don't know. I'm not 100% clear on peoples' opinion of OverlappingInstances, but I as far as I know the problems are twofold: both import-unsafeness, and the matter of how you would actually define "most specific" in a way that's both rigorous and intuitive; this would remove at least the latter.)
Anyway, thoughts? Is this all completely crazy and way out there?
[1] http://byorgey.wordpress.com/2010/08/05/typed-type-level-programming-in-hask... [2] http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
-- Work is punishment for failing to procrastinate effectively.
On 8/29/10 1:33 PM, Gábor Lehel wrote:
Another thing I'm wondering about is that there's a fairly intuitive correspondence between functions at the value level vs. functions at the type level, and datatypes to classify the value level vs. datakinds to classify the type level, but what corresponds to type classes at the value level?
Wouldn't you go the other way: kind classes? Type classes are predicates on types, and the application of a class to a type forms a proposition which represents the type of proofs that the proposition holds (i.e., the type of instance dictionaries). This can be easily extended upwards by having predicates on kinds yielding propositions that represent the kinds of (type-level) proofs. IIRC, this is the perspective that Omega takes. To extend it downward we'd have to ask what it would mean to have a predicate on values. The value-level propositions formed by applying those predicates couldn't have proofs (because there is no sub-value level), so it's not entirely clear what that would mean. If anything, the value-level correspondent of type classes are just uninterpreted predicates, i.e. data constructors. Whether this line of thinking is sensible or just a fallacious attempt to unify everything, I can't say off hand. I think it's better to think of contexts as the type of the invisible lambda for passing dictionaries, just as forall is the type of (the invisible) big-lambda, and -> is the type of lambda. Thus, the dictionaries are the concrete thing you want to generalize to higher levels; the classes will be at the next level up. -- Live well, ~wren
On Mon, Aug 30, 2010 at 1:23 PM, wren ng thornton
On 8/29/10 1:33 PM, Gábor Lehel wrote:
Another thing I'm wondering about is that there's a fairly intuitive correspondence between functions at the value level vs. functions at the type level, and datatypes to classify the value level vs. datakinds to classify the type level, but what corresponds to type classes at the value level?
Wouldn't you go the other way: kind classes? Type classes are predicates on types, and the application of a class to a type forms a proposition which represents the type of proofs that the proposition holds (i.e., the type of instance dictionaries). This can be easily extended upwards by having predicates on kinds yielding propositions that represent the kinds of (type-level) proofs. IIRC, this is the perspective that Omega takes.
To extend it downward we'd have to ask what it would mean to have a predicate on values. The value-level propositions formed by applying those predicates couldn't have proofs (because there is no sub-value level), so it's not entirely clear what that would mean. If anything, the value-level correspondent of type classes are just uninterpreted predicates, i.e. data constructors. Whether this line of thinking is sensible or just a fallacious attempt to unify everything, I can't say off hand.
I think it's better to think of contexts as the type of the invisible lambda for passing dictionaries, just as forall is the type of (the invisible) big-lambda, and -> is the type of lambda. Thus, the dictionaries are the concrete thing you want to generalize to higher levels; the classes will be at the next level up.
Hmm, I see. I think what had me confused was that type classes seem to be at the same level as types, and, like functions, to interact with things at their own level; but then they also interact with something from one level lower (instance dictionaries), which is why it doesn't make sense to transplant them to the lowest level (values). Thanks for the explanation!
-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Work is punishment for failing to procrastinate effectively.
This is probably widely known already but I just realized you can sort-of have closed classes as it is:
module SomeModule( SomeClass, someMethod ) where
class SomeClassInternal a where someMethodInternal :: a -> Integer
instance SomeClassInternal Integer where someMethodInternal = id
instance SomeClassInternal [a] where someMethodInternal = fromIntegral . length
instance SomeClassInternal Bool where someMethodInternal False = 0 someMethodInternal True = 42
class SomeClassInternal a => SomeClass a instance SomeClass Integer instance SomeClass [a] instance SomeClass Bool
someMethod :: SomeClass a => a -> Integer someMethod = someMethodInternal
Basically, not exporting a class is a very obvious way to prevent people from declaring new instances. The problem is that they also can't refer to it in any way, and if it shows up in the public API in a significant way (besides it being just weird) they have to try and manage their business without using type signatures. The solution is pretty simple: declare a private class with private methods, and a corresponding public class which implies the private one, with instances for all the same types, and have everything in the public API use the public class instead. That way people still can't declare new instances for the private class (it's not visible), nor for the public one (because they can't satisfy the superclass constraint), but otherwise they're free to use it in type signatures and do whatever they want. I don't think the compiler would use this to reason about the code in new ways (i.e. the typechecker would still treat it as open), but it's at least something. (You could also use UndecidableInstances and `instance SomeClassInternal a => SomeClass a` for less repetition and easier maintainability; the advantage of not doing so is that you don't need UndecidableInstances, and the resulting Haddocks are friendlier, especially if/when Haddock gets updated to hide instances of non-exported classes.)
participants (3)
-
Gábor Lehel -
Patrick Browne -
wren ng thornton