A foray into type-level programming, and getting stuck
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 :)
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...
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
Am Sonntag, 1. März 2009 22:10 schrieb 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").
Note that HList still needs overlapping instances for implementing type equality. If we will have closed type families at some future time, this will change. See: http://www.mail-archive.com/glasgow-haskell-users%40haskell.org/msg12792.htm... Best wishes, Wolfgang
participants (3)
-
Brian Bloniarz -
George Pollard -
Wolfgang Jeltsch