Lack of expressiveness in kinds?
Ok, so I'm inching closer to understanding monads, and this question popped up today. Consider the following 2 declarations: data Foo a = Bar a data (Ord a) => Baz a = Bah a Note that both of these have kind * -> *. However, Baz could never be an instance of monad, because there is a restriction on the types it can operate on. Foo, however, is completely polymorphic, without limitation. It seems to me that there ought to be a way to express the difference between the two in the type/kind system. For example, you can almost, but not quite, say that in the declaration "class Monad m where..", m must be of kind *->*, but that's not quite enough to say, because of this example. Am I just missing something, or is there a reason the kind of Baz shouldn't be something other than *->*?
Andrew Wagner wrote
data Foo a = Bar a data (Ord a) => Baz a = Bah a
Note that both of these have kind * -> *. However, Baz could never be an instance of monad, because there is a restriction on the types it can operate on.
There is a wide-spread opinion that one ought not to give context to a data type declaration (please search for `restricted datatypes Haskell'). Someone said that in GHC typechecker such contexts called stupidctx. There has been a proposal to remove that feature from Haskell, although I like it as a specification tool. John Hughes wrote a paper about a better use for that feature: John Hughes. 1999. Restricted datatypes in Haskell. In Proceedings of the 1999 Haskell workshop, ed. Erik Meijer. Technical Report UU-CS-1999-28, Department of Computer Science, Utrecht University. http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps That proposal has not been implemented. One should point out that restricted monads are available in Haskell right now: http://www.haskell.org/pipermail/haskell-prime/2006-February/000498.html It seems one can even use the do-notation for them, with the help of `rebindable syntax' feature of GHC. This is because the types of restricted bind and return are exactly the same as those of regular bind and return. Only the `Monad' constraint is a bit different. Restricted monads are the strict super-set of the ordinary monads, so the backwards compatibility is maintained. One almost wishes for a fuller integration of restricted monads into the language...
On 16/03/07, oleg@pobox.com
There is a wide-spread opinion that one ought not to give context to a data type declaration (please search for `restricted datatypes Haskell'). Someone said that in GHC typechecker such contexts called stupidctx. There has been a proposal to remove that feature from Haskell, although I like it as a specification tool. John Hughes wrote a paper about a better use for that feature:
I'd like to qualify this remark by adding that, to me, this opinion arises from the fact that compilers treat constraints as orthogonal to kinds, but not from the fact that constraints are a bad idea. I also want to point Andrew to the fact that constraints are not associated with the type but with (some of) the value constructors, perhaps in order to keep the kind system intact. For example, define data Eq a => Set a = MkSet [a] I'd say we need the constraint in order to define a set. Nevertheless, evaluate const 0 (undefined :: Set (Int -> Int)) Funny we can give undefined the type Set (Int -> Int) when functions have no Eq instance. Another example, define: data Eq a => Foo a = FNil | FCons a (Foo a) the type of the value constructors is : FNil :: Foo a FCons :: Eq a => a -> Foo a -> Foo a By not putting the constraint in the polymorphic value FNil we may get silly type errors when there are none. As I understand, ideally the constraint restricts the range of types to which the type constructor can be applied. Hardly a kind * -> * then, for * stands for the whole universe of types (not type constructors). Passing the potato to the value system and letting the value constructors bring up the constraints in construction or pattern matching is not the same thing. Then we have the complaint that if we want to use a constrained type then we have to place constraints in all the functions that use it, so why not put them there. In other words, instead of data Ord a => BinTree a = Leaf | Node a (BinTree a) (BinTree a) insert :: Ord a => a -> BinTree a -> BinTree a let's write: data BinTree a = Leaf | Node a (BinTree a) (BinTree a) insert :: Ord a => a -> BinTree a -> BinTree a However, I find this wrong from a formal point of view. The constraint is associated with the type, not the functions. Compare with the list type and the function sort, which has an Ord constraint which belongs to the function. There is no such thing as a constrained list *type*, only that sort takes a list with elements in ord and no other list.
From a practical point of view, if you like type inference, you may omit the constraint in the functions if it appears in one place, that is, where the type is defined. (To recall, John Hugues paper begins with the complaint that changing the constraint in the type affects the type signatures of functions when written explicitly.)
The solution perhaps is not to ignore constraints and treat them as a minor evil, but to make them an integral part of the type system, as entities that can be passed as arguments and returned as results at the type level. And also as parameters to class declarations. A questionable implementation decision should not be the origin of a recommended style of programming.
participants (3)
-
Andrew Wagner -
oleg＠pobox.com -
Pablo Nogueira