[Haskell-cafe] GADT and instance deriving

[Richard Eisenberg]

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
  ElectricField :: Operation '[One, Zero] One
  GravitationalField :: Operation '[Zero] One

opToString :: Operation a b -> String
opToString ElectricField = "E"
opToString GravitationalField = "G"

data HList :: [Nat] -> * where
  HNil :: HList '[]
  HCons :: Tensor head -> HList tail -> HList (head ': tail)

data Tensor :: Nat -> * where
  Tensor :: Operation operands result -> HList operands -> Tensor result
----

The idea here is that a well-typed operands list is intimately tied to the choice of operation. So, we must somehow expose the required operands in our choice of operation. The Operation GADT does this for us. (It is still easy to recover string representations, as in opToString.) Then, in the type of the Tensor constructor, we say that the operands must be appropriate for the operation. Note that `operands` is still existential in the Tensor constructor, but I believe that is what you want.

Does this work for you?

I will repeat that others will likely say that this approach is *too* strongly-typed, that the types are getting in the way of the programmer. There is merit to that argument, to be sure. However, I still believe that using a detailed, strongly-typed interface will lead sooner to a bug-free program than the alternative. Getting your program to compile and run the first time may take longer with a strongly-typed interface, but I posit that it will have fewer bugs and will be ready for "release" (whatever that means in your context) sooner.

Richard

On May 25, 2013, at 10:23 AM, TP wrote:

> 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 Tensor :: Nat -> * where
> [...]
>    Tensor :: String -> [IndependentVar] -> Tensor order
> [...]
> ------------
> 
> The idea is that, for example, I may have a vector function of time and 
> position, for example the electric field:
> 
> E( r, t )
> 
> (E: electric field, r: position vector, t: time)
> 
> So, I have a Tensor (E) that depends on two tensors (r and t). I want to put 
> r and t in a list, the list of independent variable of which E is a 
> function. But we see immediately that r and t have not the same type: the 
> first is of type "Tensor One", the second of type "Tensor Zero". Thus we 
> cannot put them in a list. This is why I have tried to use an heterogeneous 
> list:
> 
> http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:_heterogeneous_lists
> 
> Thus in the first place the problem comes from the fact that I have put the 
> order of the Tensor in the type rather than in the data constructors. But it 
> is useful:
> 
> * I can make type synonyms
> type Scalar = Tensor Zero
> type Vector = Tensor One
> [...]
> 
> * with multi-parameter typeclasses, I can define operations as:
> 
> class Division a b c | a b -> c where
>     (/) :: a -> b -> c
> 
> and then I implement these operations on a subset of types:
> 
> instance (PrettyPrint (Tensor a)) => Division (Tensor a) Scalar (Tensor a) 
> where
>   ZeroTensor / _ = ZeroTensor
>   _ / ZeroTensor = error "Division by zero!"
>   t / s = Divide t s
> 
> So, the code is clear, and instead of runtime dimension checks, everything 
> is detected at compilation. So the choice of putting the order in the type 
> seems to be correct.
> My only need to use Typeable comes from the heterogeneous list. But how to 
> do without?
> 
> Thanks,
> 
> TP
> 
> 
> 
> Richard Eisenberg wrote:
> 
>> 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
>> compiler working, see here:
>> http://hackage.haskell.org/trac/ghc/wiki/Building
>> 
>> However, I'm worried that other aspects of your design may be suboptimal.
>> The `Box` type you mentioned a few posts ago is called an existential
>> type. Existential types have constructors who have type parameters that
>> are *not* mentioned in the conclusion. As an example, your `Box`
>> constructor involved a type parameter `a`, but the `Box` type itself has
>> no parameters. This existential nature of the type is why your comparison
>> didn't work.
>> 
>> A Tensor, however, doesn't seem like it would need to be an existential
>> type. The order of the tensor should probably (to my thinking) appear in
>> the type, making it not existential anymore.
>> 
>> In general, I (personally -- others will differ here) don't love using
>> Typeable. By using Typeable, you are essentially making a part of your
>> program dynamically typed (i.e., checked at runtime). The beauty of
>> Haskell (well, one of its beauties) is how it can check your code
>> thoroughly at compile time using its rich type language. This prevents the
>> possibility of certain bugs at runtime. Using Typeable circumvents some of
>> that, so I would recommend thinking carefully about your design to see if
>> its use can be avoided.
>> 
>> Just to diffuse any flames I get for the above paragraph: I fully support
>> the role of Typeable within Haskell. Indeed, sometimes it is unavoidable.
>> In fact, I have a small update to the Typeable interface on my to-do list
>> (adding functionality, not changing existing). I am just arguing that its
>> use should be judicious.
> 
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe