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