[TYPES] seeking correct term for a quasi-dependent type

[Tim Sweeney]

Norman,

I'd say Info is a "type-indexed type", so outputFact is a "type-indexed function".  I see a type-indexed type is weaker than:

* A "type-dependent type" -- which implies a richer mechanism for expressing dependencies beyond case decomposition by exact-match of types.

* A "value-dependent type" -- e.g. natural numbers less than i, for a non-constant natural number variable i.

* A dependent type, allowing mixing and matching dependency on types and values.

Tim Sweeney
Epic Games

________________________________________
From: types-list-bounces at lists.seas.upenn.edu [types-list-bounces at lists.seas.upenn.edu] On Behalf Of Norman Ramsey [nr at cs.tufts.edu]
Sent: Thursday, June 10, 2010 2:00 PM
To: types-list at lists.seas.upenn.edu
Cc: nr at cs.tufts.edu
Subject: [TYPES] seeking correct term for a quasi-dependent type

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

A new feature of the Glasgow Haskell Compiler, called 'indexed type
families', makes it possible to write something that isn't a true
dependent type but isn't parametrically polymorphic either.
I'd like help figuring out what to call it.  Here's an
example that is pretty close to what we're actually doing:

  outputFact :: forall a . a -> Info a

Although 'Info' has the same syntax as a parametric type
*constructor*, it is actually a *partial* *function* on types:

  data Fact   = ...
  data Middle = ...
  data Last   = ...
  newtype Label = Label Int

  -- here follows the definition of 'Info':
  type family   Info a :: *
  type instance Info Middle = Fact
  type instance Info Last   = [(Label, Fact)]

How do I describe the function 'outputFact'?
It's not a classic dependent function, because the type of the result
doesn't depend on the value of the argument.  But the type of the
result *does* depend on the static *type* of the argument.

And outputFact is less polymorphic than it might appear, since the
bound type variable 'a' cannot be instantiated at any type, but only
at a type in the domain of the type function 'Info'.

I'm a little reluctant to call 'outputFact' a "dependent function"
or to say that it has a "dependent-function type", because those
words mean something else.  But I'm at a loss as to how to describe it.

What sort of type is the type

  forall a . a  -> Info a

?



Norman