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

[Brian Bloniarz]

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

_________________________________________________________________
Windows Live™: Life without walls.
http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009