Re: [Haskell-cafe] GADT and instance deriving

I don't yet see a problem with the strongly-typed approach. Following the code I posted previously, for your deriv function, you would need sommething like the following: --- deriv :: (HList indeps -> Tensor result) -> (HList (DerivIndeps indeps result) -> Tensor (DerivResult indeps result)) t

Re: [Haskell-cafe] GADT and instance deriving

Hi Tillmann and Richard, Thanks for your answers. I have tried to analyze the code snippets you proposed. I've tried to transpose your examples to what I need, but it is not easy. The problem I see with putting the list of independent variables (*) at the type level is that at some time in my c

Re: [Haskell-cafe] GADT and instance deriving

Would this work for you? {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators #-} data Nat = Zero | Succ Nat type One = Succ Zero type Two = Succ One data Operation :: [Nat] -- list of operand orders -> Nat -- result order -> * where Electri

Re: [Haskell-cafe] GADT and instance deriving

Hi, TP wrote: Today I have a type constructor "Tensor" in which there is a data constructor Tensor (among others): data Tensor :: Nat -> * where [...] Tensor :: String -> [IndependentVar] -> Tensor order [...] The idea is that, for example, I may have a vector fu

Re: [Haskell-cafe] GADT and instance deriving

Hi Richard, Thanks a lot for your answer. We had a discussion about some "Tensor" type some time ago: https://groups.google.com/d/msg/haskell-cafe/Rh65kdPkX70/T2zZpV6ZpjoJ Today I have a type constructor "Tensor" in which there is a data constructor Tensor (among others): data Ten

Re: [Haskell-cafe] GADT and instance deriving

Hi TP, Thankfully, the problem you have is fixed in HEAD -- the most recent version of GHC that we are actively working on. I am able, using the HEAD build of GHC, to use a `deriving Typeable` annotation to get a Typeable instance for a type that has non-*-kinded parameters. To get the HEAD com

Re: [Haskell-cafe] GADT and instance deriving

TP wrote: > Where are these examples that can help me to write my instance? > I have tried to read the source of the implemented instances in > data.typeable, not so easy for me. Ok, by doing a better search on Google ("instance typeable " blog), I have found interesting information: http://blo

Re: [Haskell-cafe] GADT and instance deriving

On 25/05/13 06:06, Alexander Solla wrote: > On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen > wrote: > > On Sat 25 May 2013 00:37:59 SGT, TP wrote: > > Is this the right way to go? Is there any other solution? > > I believe whether it's right or just depends

Re: [Haskell-cafe] GADT and instance deriving

Alexander Solla wrote: >> (Do you confirm that tilde in s~s1 means "s has the same type as s1"? I >> have >> not found this information explicitly in the Haskell stuff I have read). >> > > Yes. > > http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/equality-constraints.html > > Is this (Typ

Re: [Haskell-cafe] GADT and instance deriving

On Fri, May 24, 2013 at 9:37 AM, TP wrote: > Hello, > > I continue my learning of "not so obvious" Haskell/GHC topics when > encountering problems in the code I write. > Below is a small example of an heterogeneous list, using GADT, inspired > from: > > http://en.wikibooks.org/wiki/Haskell/Existe

Re: [Haskell-cafe] GADT and instance deriving

On Fri, May 24, 2013 at 10:41 AM, Niklas Hambüchen wrote: > On Sat 25 May 2013 00:37:59 SGT, TP wrote: > > Is this the right way to go? Is there any other solution? > > I believe whether it's right or just depends on what you want to express. > > > Do you confirm that tilde in s~s1 means "s has t

Re: [Haskell-cafe] GADT and instance deriving

On Sat 25 May 2013 00:37:59 SGT, TP wrote: > Is this the right way to go? Is there any other solution? I believe whether it's right or just depends on what you want to express. > Do you confirm that tilde in s~s1 means "s has the same type as s1"? It means: Both your s and s1 are "Eq"s but not n