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 :)
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe