[Haskell-cafe] Re: A type class puzzle

[Chung-chieh Shan]

Yitzchak Gale <gale at sefer.org> wrote in article <2608b8a80610310102i1e54092bhb04da958a3978def at mail.gmail.com> in gmane.comp.lang.haskell.cafe:
> 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