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

[Brian Bloniarz]

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-cns!503D1D86EBB2B53C!2285.entry?ocid=TXT_TAGLM_WL_UGC_Contacts_032009