
Yitzchak Gale
replace0 :: a -> a -> a replace1 :: Int -> a -> [a] -> [a] replace2 :: Int -> Int -> a -> [[a]] -> [[a]]
This message is joint work with Oleg Kiselyov. All errors are mine. Part of what makes this type-class puzzle difficult can be explained by trying to write Prolog code to identify those types that the general "replace" function can take. We use an auxiliary predicate repl(X0,X,Y0,Y), which means that X0 is "int ->" applied the same number of times to X as Y0 is "[]" applied to Y. repl(X, X, Y, Y). repl((int -> X0), X, [Y0], Y) :- repl(X0, X, Y0, Y). We can now write a unary predicate replace1(X0) to test if any given type X0 is a valid type for the "replace" function. replace1(X0) :- repl(X0, (Y -> Y0 -> Y0), Y0, Y). Positive and negative tests: ?- replace1(bool -> bool -> bool). ?- replace1(int -> bool -> [bool] -> [bool]). ?- replace1(int -> int -> bool -> [[bool]] -> [[bool]]). ?- replace1(int -> int -> int -> [[int]] -> [[int]]). ?- \+ replace1(bool -> [bool] -> [bool]). The optimist would expect to be able to turn these Prolog clauses into Haskell type-class instances directly. Unfortunately, at least one difference between Prolog and Haskell stands in the way: Haskell overloading resolution does not backtrack, and the order of type-class instances should not matter. Suppose that we switch the two repl clauses and add a cut, as follows: repl((int -> X0), X, [Y0], Y) :- !, repl(X0, X, Y0, Y). repl(X, X, Y, Y). Now the second-to-last test above ?- replace1(int -> int -> int -> [[int]] -> [[int]]). fails, because repl needs to "look ahead" beyond the current argument type to know that the third "int" in the type is not an index but a list element. This kind of ambiguity is analogous to a shift-reduce conflict in parsing. We could roll our own backtracking if we really wanted to, but let's switch to the saner type family
replace0 :: a -> a -> a replace1 :: Int -> [a] -> a -> [a] replace2 :: Int -> Int -> [[a]] -> a -> [[a]]
where the old list comes before the new element. The corresponding Prolog predicate and tests now succeed, even with the switched and cut repl clauses above. replace2(X0) :- repl(X0, (Y0 -> Y -> Y0), Y0, Y). ?- replace2(bool -> bool -> bool). ?- replace2(int -> [bool] -> bool -> [bool]). ?- replace2(int -> int -> [[bool]] -> bool -> [[bool]]). ?- replace2(int -> int -> [[int]] -> int -> [[int]]). ?- \+ replace2([bool] -> bool -> [bool]). Regardless of this change, note that a numeric literal such as "2" in Haskell can denote not just an Int but also a list, given a suitable Num instance. Therefore, the open-world assumption of Haskell type classes forces us to annotate our indices with "::Int" in Haskell. Below, then, are the tests that we strive to satisfy.
x1 = "abc" x2 = ["ab", "cde", "fghi", "uvwxyz"] x3 = [[[i1 + i2 + i3 | i3 <- [10..13]] | i2<- [4..5]] | i1 <- [(1::Int)..3]]
test1:: String test1 = replace (1::Int) x1 'X'
{- expected error reported test2:: [String] test2 = replace (1::Int) x2 'X' -}
test3:: [String] test3 = replace (1::Int) x2 "X"
test4:: [String] test4 = replace (2::Int) (1::Int) x2 'X'
test5:: [[[Int]]] test5 = replace (2::Int) (0::Int) (1::Int) x3 (100::Int)
The remainder of this message shows two ways to pass these tests. Both ways require allowing undecidable instances in GHC 6.6.
{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}
In the first way, the Replace type-class parses the desired type for "replace" into a tuple of indices, in other words, a type-level list of indices. An auxiliary type-class Replace' then reverses this list. Finally, another auxiliary type-class Replace'' performs the actual replacement.
class Replace'' n old new where repl'' :: n -> old -> new -> old instance Replace'' () a a where repl'' () old new = new instance Replace'' n old new => Replace'' (n,Int) [old] new where repl'' (i,i0) old new = case splitAt i0 old of (h,[] ) -> h (h,th:tt) -> h ++ repl'' i th new : tt
class Replace' n n' old new where repl' :: n -> n' -> old -> new -> old instance Replace'' n old new => Replace' n () old new where repl' n () = repl'' n instance Replace' (n1,n2) n3 old new => Replace' n1 (n2,n3) old new where repl' n1 (n2,n3) = repl' (n1,n2) n3
class Replace n a b c where repl :: n -> a -> b -> c instance Replace' () n [old] new => Replace n [old] new [old] where repl = repl' () instance Replace (i,n) a b c => Replace n i a (b->c) where repl i0 i = repl (i,i0)
replace n = repl () n
The second way, shown below, eliminates the intermediate tuple of indices used above. This code doesn't require allowing undecidable instances in Hugs, but it does use functional dependencies to coax Haskell into applying the last Replace instance.
class Replace old new old' new' w1 w2 w3 | w1 w2 w3 -> old new old' new' where repl :: ((old -> new -> old) -> (old' -> new' -> old')) -> w1 -> w2 -> w3 instance Replace a a b a b a b where repl k = k (\old new -> new) instance Replace old new old' new' w1 w2 w3 => Replace [old] new old' new' Int w1 (w2 -> w3) where repl k i = repl (\r -> k (\old new -> case splitAt i old of (h, [] ) -> h (h, th:tt) -> h ++ r th new : tt))
replace :: Replace old new old new w1 w2 w3 => w1 -> w2 -> w3 replace = repl id
Both ways pass all tests above. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig The fact that SM [Standard Model] cannot suggest any reason for our continued existence seems to be pretty serious to me. Discussion on Ars Technica about barion counts, mesons and SM