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

[Wolfgang Jeltsch]

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:



Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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




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