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