Actually, it's not necessary to remove the overlap, it's enough to add the ImplementsPrev constraint:
instance (Pred x x', Nthable b x' r, ImplementsPrev (Tuple n a b) x) ⇒ Nthable (Tuple n a b) x r where nth _ (Tuple _ b) = nth (undefined ∷ x') b
It looks like this typechecks too -- the only thing overlap-free did was to make the error message clearer. -Brian
Hi George,
Since none of the type metaprogramming specialists have answered you on-list, I took a crack at this -- I think you can work around the issue by avoiding overlapping instances entirely. I learned about this technique from the HList paper & this message: http://okmij.org/ftp/Haskell/keyword-arguments.lhs (see "the rest of the implementation").
I'm not sure it's the simplest approach, but it works for me. To avoid overlap in ImplementsPrev t n, use type-level's comparison class (Trich) to compare n to D1:
class (Pos n) ⇒ ImplementsPrev t n instance (Trich n D1 cmpD1, ImplementsPrev' cmpD1 t n) ⇒ ImplementsPrev t n
Now, the auxiliary class ImplementsPrev' can be non-overlapping because it dispatches on the result of (Trich n D1):
class (Pos n) ⇒ ImplementsPrev' cmpD1 t n instance (Pred n n', Nthable t n' a) ⇒ ImplementsPrev' GT t n instance ImplementsPrev' EQ t D1
I needed one more change to make it work, including the ImplementsPrev constraint in the Nthable instance.
instance (Pred x x', Nthable b x' r, ImplementsPrev (Tuple n a b) x) ⇒ Nthable (Tuple n a b) x r where nth _ (Tuple _ b) = nth (undefined ∷ x') b I'm not sure why this is needed.
Hope this helps, -Brian
Okay, so I've written a small library to generalize 'fst' and 'snd' to arbitrary tuples, but I'd like to extend it a bit. I'm using the type-level library to do the thinking :)
Imports and defines first:
{-# LANGUAGE UnicodeSyntax, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, DeriveDataTypeable, OverlappingInstances, ScopedTypeVariables #-} import Prelude hiding ((-),Eq) import qualified Prelude as P import Data.TypeLevel.Num.Sets import Data.TypeLevel.Num.Reps import Data.TypeLevel.Num.Aliases import Data.TypeLevel.Bool import Data.TypeLevel.Num.Ops import Data.Typeable
I start by requiring that if you can access element 'n', you should be able to access element 'n-1'.
class (ImplementsPrev t n a) ⇒ Nthable t n a | t n → a where nth ∷ n → t → a
class (Pos n) ⇒ ImplementsPrev t n a instance (Pred n n', Nthable t n' a') ⇒ ImplementsPrev t n a instance ImplementsPrev t D1 a
So, this is a simple induction. Testing it with the nthable instances confirms that it works; removing either of the first two lines stops the code from compiling, hurrah!
instance Nthable (a,b,c) D1 a where nth _ (a,_,_) = a instance Nthable (a,b,c) D2 b where nth _ (_,b,_) = b instance Nthable (a,b,c) D3 c where nth _ (_,_,c) = c
Now, I have heard talk/suggestions of revamping tuples in Haskell to a more flexible system. Perhaps we would like to do it like this (modulo strictness annotations):
data (Nat n) ⇒ Tuple n a b = Tuple a b deriving (Show,Read,Typeable,P.Eq,Ord) infixr 0 `comma` -- comma :: a -> (b ~> c) -> (a ~> (b ~> c)) -- to investigate comma ∷ (Succ n n') ⇒ a → Tuple n b c → Tuple n' a (Tuple n b c) x `comma` y = Tuple x y empty ∷ Tuple D0 () undefined empty = Tuple () undefined
Thus, we can create, e.g. (1 `comma` 2 `comma` empty). Now, I'd like to be able to write Nthable instances, so I start with the base case:
instance (n :>=: D1) ⇒ Nthable (Tuple n a b) D1 a where nth _ (Tuple a _) = a
This works well. However, I am really stuck on the instance for the inductive case. My first idea was this:
instance (Pred x x', Nthable b x' r) ⇒ Nthable (Tuple n a b) x r where nth _ (Tuple _ b) = nth (undefined ∷ x') b
But this doesn't work, muttering about IncoherentInstances and hidden datatypes from the type-level library.
So, I turn to Haskell café for help :)
_________________________________________________________________ Windows Live™ Contacts: Organize your contact list. http://windowslive.com/connect/post/marcusatmicrosoft.spaces.live.com-Blog-c...
_________________________________________________________________ Windows Live™: Life without walls. http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009