Re: [Haskell-cafe] typeclass to select a list element

2013-10-12 Thread Paolino 
Hello everyone,

I'm still trying to resolve my problem. I try to restate it in a simpler
way.
Is it possible to write extract and update functions for L ?

import Data.Nat

data family X (n::Nat) :: *

data L (n::Nat) where
Q :: L (Succ n) - X n - L n
E :: L n

extract :: L Zero - X n
extract = undefined

update :: L Zero - (X n - X n) - L Zero
update = undefined

Thanks for hints and help

paolino



2013/10/7 Paolino paolo.verone...@gmail.com

 Hello, I'm trying to use a type class to select an element from a list.
 I would like to have a String CC as a value for l10'.


 {-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds
 ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances,
 StandaloneDeriving, UndecidableInstances #-}



 import Data.Nat
 import Data.Monoid

 data family X (n::Nat) :: *

 data L (n::Nat) where
 Q :: (Monoid (X n), Show (X n)) = L (Succ n) - X n - L n
 E :: Monoid (X n) = L n

 deriving instance Show (L n)
 data instance X n = String String

 instance Monoid (X n) where
 String x `mappend` String y = String $ x `mappend` y
 mempty = String 
 deriving instance Show (X n)

 class Compose n n' where
 compose :: L n  - L n  - X n'

 instance Compose n n where
 compose (Q _ x) (Q _ y) = x `mappend` y
 compose _ _ = mempty

 instance Compose n n' where
 compose (Q x _) (Q y _) = compose x y
 compose _ _ = mempty

 l0 :: L Zero
 l0 = Q (Q E $ String C) $ String A

 l0' :: L Zero
 l0' = Q (Q E $ String C) $ String B


 l10' :: X (Succ Zero)
 l10' = compose l0 l0'

 l00' :: X Zero
 l00' = compose l0 l0'
 {-

 *Main l00'
 String AB
 *Main l10'
 String 

 -}

 Thanks for help.

 paolino

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

Re: [Haskell-cafe] typeclass to select a list element

2013-10-12 Thread adam vogt 
Hi Paolino,

There are some functions similar to that in HList (Data.HList.HArray).
Check the repo http://code.haskell.org/HList for a version that uses
more type families / gadts.

Maybe there is a way to take advantage of the fact that you've
labelled the elements of the list, but extract isn't too bad if you
don't: http://lpaste.net/94210.

Regards,
Adam

On Sat, Oct 12, 2013 at 4:41 AM, Paolino paolo.verone...@gmail.com wrote:
 Hello everyone,

 I'm still trying to resolve my problem. I try to restate it in a simpler
 way.
 Is it possible to write extract and update functions for L ?

 import Data.Nat


 data family X (n::Nat) :: *

 data L (n::Nat) where
 Q :: L (Succ n) - X n - L n
 E :: L n

 extract :: L Zero - X n
 extract = undefined

 update :: L Zero - (X n - X n) - L Zero
 update = undefined

 Thanks for hints and help

 paolino



 2013/10/7 Paolino paolo.verone...@gmail.com

 Hello, I'm trying to use a type class to select an element from a list.
 I would like to have a String CC as a value for l10'.


 {-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds
 ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances,
 StandaloneDeriving, UndecidableInstances #-}



 import Data.Nat
 import Data.Monoid

 data family X (n::Nat) :: *

 data L (n::Nat) where
 Q :: (Monoid (X n), Show (X n)) = L (Succ n) - X n - L n
 E :: Monoid (X n) = L n

 deriving instance Show (L n)
 data instance X n = String String

 instance Monoid (X n) where
 String x `mappend` String y = String $ x `mappend` y
 mempty = String 
 deriving instance Show (X n)

 class Compose n n' where
 compose :: L n  - L n  - X n'

 instance Compose n n where
 compose (Q _ x) (Q _ y) = x `mappend` y
 compose _ _ = mempty

 instance Compose n n' where
 compose (Q x _) (Q y _) = compose x y
 compose _ _ = mempty

 l0 :: L Zero
 l0 = Q (Q E $ String C) $ String A

 l0' :: L Zero
 l0' = Q (Q E $ String C) $ String B


 l10' :: X (Succ Zero)
 l10' = compose l0 l0'

 l00' :: X Zero
 l00' = compose l0 l0'
 {-

 *Main l00'
 String AB
 *Main l10'
 String 

 -}

 Thanks for help.

 paolino



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

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

Re: [Haskell-cafe] ordNub

2013-10-12 Thread Niklas Hambüchen 
I would like to come back to the original question:

How can ordNub be added to base?

I guess we agree that Data.List is the right module for a function of
type Ord a = [a] - [a], but this introduces

* a cyclic dependency between Data.List and Data.Set
* a base dependency on containers.

What is the right way to go with that?

Should ordNub be introduced as part of Data.Set, as Conrad suggested?

It does not really have anything to do with Set, apart from being
implemented with it.

On 14/07/13 14:12, Roman Cheplyaka wrote:
 Something like that should definitely be included in Data.List.
 Thanks for working on it.
 
 Roman
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] ordNub

2013-10-12 Thread Anthony Cowley 

On Oct 12, 2013, at 2:47 PM, Niklas Hambüchen m...@nh2.me wrote:
 
 I would like to come back to the original question:
 
 How can ordNub be added to base?
 
 I guess we agree that Data.List is the right module for a function of
 type Ord a = [a] - [a], but this introduces
 
 * a cyclic dependency between Data.List and Data.Set
 * a base dependency on containers.
 
 What is the right way to go with that?
 
 Should ordNub be introduced as part of Data.Set, as Conrad suggested?
 
 It does not really have anything to do with Set, apart from being
 implemented with it.

I think nub's behavior is rather set-related, so I don't really understand the 
objection to putting it in Data.Set.

Anthony

 
 On 14/07/13 14:12, Roman Cheplyaka wrote:
 Something like that should definitely be included in Data.List.
 Thanks for working on it.
 
 Roman
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] ordNub

2013-10-12 Thread Niklas Hambüchen 
On 12/10/13 20:43, Anthony Cowley wrote:
 I think nub's behavior is rather set-related, so I don't really understand 
 the objection to putting it in Data.Set.

In sets, the order does not matter, while for nub it does.

nub:: Eq a  = [a] - [a]
ordNub :: Ord a = [a] - [a]

both do not mention Set, and the fact that Set is used inside my
proposed ordNub implementation is a detail not visible to the caller.

That's why it looks like a Data.List function to me.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] ordNub

2013-10-12 Thread Roman Cheplyaka 
* Anthony Cowley acow...@seas.upenn.edu [2013-10-12 15:43:57-0400]
 
 On Oct 12, 2013, at 2:47 PM, Niklas Hambüchen m...@nh2.me wrote:
  
  I would like to come back to the original question:
  
  How can ordNub be added to base?
  
  I guess we agree that Data.List is the right module for a function of
  type Ord a = [a] - [a], but this introduces
  
  * a cyclic dependency between Data.List and Data.Set
  * a base dependency on containers.
  
  What is the right way to go with that?
  
  Should ordNub be introduced as part of Data.Set, as Conrad suggested?
  
  It does not really have anything to do with Set, apart from being
  implemented with it.
 
 I think nub's behavior is rather set-related, so I don't really
 understand the objection to putting it in Data.Set.

It's not Set (in the data structure sense) related. It's list-related,
because it clearly acts on lists.

Therefore, it belongs to Data.List.

Besides, we already have the precedent of the slow nub being in
Data.List.

Roman


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Haskellers in Nashville,TN

2013-10-12 Thread heathmatlock 
Anyone here from the Nashville, TN area? t would be nice to meet
regularly with others to discuss and work with Haskell. Also, this
group is now available:

www.meetup.com/The-Haskell-Study-Group/

If you want to participate remotely, that works too, I'm just looking
for others to meet with regularly.

-- 
Heath Matlock
+1 256 274 4225
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] typeclass to select a list element

2013-10-12 Thread Richard Eisenberg 
Yes, it's possible, but it's rather painful.

Here is my working attempt, written to be compatible with GHC 7.6.3. Better 
ones may be possible, but I'm doubtful.

 {-# LANGUAGE TemplateHaskell, RankNTypes, TypeFamilies, TypeOperators,
  DataKinds, ScopedTypeVariables, GADTs, PolyKinds #-}
 
 module ListNat where
 
 import Data.Singletons
 
 $(singletons [d|
   data Nat = Zero | Succ Nat deriving Eq
   |])
 
 -- in HEAD, these next two are defined in Data.Type.Equality
 data a :~: b where
   Refl :: a :~: a
 
 gcastWith :: (a :~: b) - ((a ~ b) = r) - r
 gcastWith Refl x = x
 
 -- functionality that subsumes this will be in the next release of singletons
 reifyNatEq :: forall (m :: Nat) (n :: Nat). ((m :==: n) ~ True, SingI m, 
 SingI n) = m :~: n
 reifyNatEq =
   case (sing :: Sing m, sing :: Sing n) of
 (SZero, SZero) - Refl
 (SSucc (_ :: Sing m'), SSucc (_ :: Sing n')) -
   gcastWith (reifyNatEq :: (m' :~: n')) Refl
 _ - bugInGHC   -- this is necessary to prevent a spurious warning from 
 GHC
 
 data family X (n::Nat) :: * 
 
 data L (n::Nat) where
 Q :: L (Succ n) - X n - L n 
 E :: L n
 
 extract :: SingI n = L Zero - X n
 extract = aux
   where
 aux :: forall m n. (SingI m, SingI n) = L m - X n
 aux list =
   case ((sing :: Sing m) %==% (sing :: Sing n), list) of
 (_,  E) - error Desired element does not exist
 (STrue,  Q _ datum) - gcastWith (reifyNatEq :: (m :~: n)) datum
 (SFalse, Q rest _)  - aux rest
 
 update :: forall n. SingI n = L Zero - (X n - X n) - L Zero
 update list upd = aux list
   where
 aux :: forall m. SingI m = L m - L m
 aux list =
   case ((sing :: Sing m) %==% (sing :: Sing n), list) of
 (_, E) - error Desired element does not exist
 (STrue, Q rest datum) - gcastWith (reifyNatEq :: (m :~: n)) (Q rest 
 (upd datum))
 (SFalse, Q rest datum) - Q (aux rest) datum

Why is this so hard? There are two related sources of difficulty. The first is 
that `extract` and `update` require *runtime* information about the *type* 
parameter `n`. But, types are generally erased during compilation. So, the way 
to get the data you need is to use a typeclass (as your subject line suggests). 
The other source of difficulty is that you need to convince GHC that you've 
arrived at the right element when you get there; otherwise, your code won't 
type-check. The way to do this is, in my view, singletons.

For better or worse, your example requires checking the equality of numbers at 
a value other than Zero. The singletons library doesn't do a great job of this, 
which is why we need the very clunky reifyNatEq. I'm hoping to add better 
support for equality-oriented operations in the next release of singletons.

I'm happy to explain the details of the code above, but it might be better as 
QA instead of me just trying to walk through it -- there's a lot of gunk to 
stare at there!

I hope this helps,
Richard


On Oct 12, 2013, at 4:41 AM, Paolino wrote:

 Hello everyone,
 
 I'm still trying to resolve my problem. I try to restate it in a simpler way.
 Is it possible to write extract and update functions for L ?
 
 import Data.Nat
 
 data family X (n::Nat) :: * 
 
 data L (n::Nat) where
 Q :: L (Succ n) - X n - L n 
 E :: L n
 
 extract :: L Zero - X n
 extract = undefined
 
 update :: L Zero - (X n - X n) - L Zero
 update = undefined
 
 Thanks for hints and help
 
 paolino
 
 
 
 2013/10/7 Paolino paolo.verone...@gmail.com
 Hello, I'm trying to use a type class to select an element from a list.
 I would like to have a String CC as a value for l10'.
 
 
 {-# LANGUAGE MultiParamTypeClasses, GADTs,FlexibleInstances,  DataKinds 
 ,TypeFamilies, KindSignatures, FlexibleContexts, OverlappingInstances, 
 StandaloneDeriving, UndecidableInstances #-}
 
 
 
 import Data.Nat
 import Data.Monoid
 
 data family X (n::Nat) :: * 
 
 data L (n::Nat) where
 Q :: (Monoid (X n), Show (X n)) = L (Succ n) - X n - L n 
 E :: Monoid (X n) = L n
 
 deriving instance Show (L n)
 data instance X n = String String
 
 instance Monoid (X n) where
 String x `mappend` String y = String $ x `mappend` y
 mempty = String 
 deriving instance Show (X n)
 
 class Compose n n' where
 compose :: L n  - L n  - X n'
 
 instance Compose n n where
 compose (Q _ x) (Q _ y) = x `mappend` y
 compose _ _ = mempty
 
 instance Compose n n' where
 compose (Q x _) (Q y _) = compose x y 
 compose _ _ = mempty
 
 l0 :: L Zero
 l0 = Q (Q E $ String C) $ String A 
 
 l0' :: L Zero
 l0' = Q (Q E $ String C) $ String B 
 
 
 l10' :: X (Succ Zero)
 l10' = compose l0 l0'
 
 l00' :: X Zero
 l00' = compose l0 l0'
 {-
 
 *Main l00'
 String AB
 *Main l10'
 String 
 
 -}
 
 Thanks for help.
 
 paolino
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe