[Haskell-cafe] GADT and instance deriving

[Tillmann Rendel]

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 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.

I don't know what a tensor is, but maybe you have to track *statically* 
what independent variables a tensor is a function of, using something like:

   E :: R -> T -> Tensor ...

or

   E :: Tensor (One -> Zero -> ...)

or

   E :: Tensor '[One, Zero] ...



I have two simple pointers to situations where something similar is 
going on. First, see the example for type-level lists in the GHC user's 
guide:

http://www.haskell.org/ghc/docs/latest/html/users_guide/promotion.html#promoted-lists-and-tuples

> data HList :: [*] -> * where
>   HNil  :: HList '[]
>   HCons :: a -> HList t -> HList (a ': t)

In this example, an HList is an heterogenous list, but it doesn't use 
existential types. Instead, we know statically what the types of the 
list elements are, because we have a type-level list of these element types.


And the second situation: The need for such type-level lists also shows 
up when you try to encode well-typed lambda terms as a datatype. You 
have to reason about the free variables in the term and their type. For 
example, the constructor for lambda expressions should remove one free 
variable from the term. You can encode this approximately as follows:

>   data Type = Fun Type Type | Num
>
>   data Term :: [Type] -> Type -> * where
>     -- arithmetics
>     Zero :: Term ctx 'Num
>     Succ :: Term ctx 'Num -> Term ctx 'Num
>     Add :: Term ctx 'Num -> Term ctx 'Num -> Term ctx 'Num
>
>     -- lambda calculus
>     App :: Term ctx ('Fun a b) -> Term ctx a -> Term ctx b
>     Lam :: Term (a ': ctx) b -> Term ctx ('Fun a b)
>     Var :: Var ctx a -> Term ctx a
>
>   -- variables
>   data Var :: [Type] -> Type -> * where
>     This :: Var (a ': ctx) a
>     That :: Var ctx a -> Var (b ': ctx) a

The point is: We know statically what free variables a term can contain, 
similarly to how you might want to know statically the independent 
variables of your tensor.

   Tillmann