[Haskell-cafe] A foray into type-level programming, and getting stuck

[George Pollard]

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 :)


-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: This is a digitally signed message part
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090227/e40dc2f9/attachment.bin