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

[Dan Doel]

On Thursday 10 June 2010 2:00:20 pm Norman Ramsey wrote:
> 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

Are you certain functions with that type are not parametric? I can only think 
of one (or two, depending on seq):

  undefined -- \_ -> undefined

You will get errors if you try to instantiate 'a' to a type without an 
instance, but the definition is parametric. The only ways you can create non-
trivial functions of the type are:

1) Type classes

  class OutputFact a where
    outputFact :: a -> Info a

  instance OutputFact Middle where ...

2) GADTs

  data T a where
    M :: T Middle
    L :: T Last

  outputFact :: forall a. T a -> a -> Info a
  outputFact M x = ...
  outputFact L x = ...

But neither of those functions has the type 'forall a. a -> Info a'. The 
former has a constraint signaling its use of type-case, and the latter has the 
GADT parameter (I'm still not certain how to think about GADTs with regard to 
parametricity, though). And it is necessary to use one of these two methods 
(or write at a specific, concrete type), because without knowing what 'a' is, 
your function cannot know what 'Info a' is, so undefined will be the only 
value available for it to produce.

Info itself is not parametric (using a somewhat generalized notion of 
parametricity; the usual one applies to value-level functions, I believe), but 
neither is 'data Id a = Id a' if you really get into it.

--

As for how to describe things like Info, type families are like defining types 
by recursion. You see this in dependently typed languages. For instance, 
vectors can be defined by recursion over the size index:

  Vec : Type -> Nat -> Type
  Vec A z     = Unit
  Vec A (s n) = A * Vec A n

the oddities are that:

1) type families are open and partial
2) type families are using recursion over *types*, whereas you can't do that 
(directly) in most dependently typed languages, since types themselves aren't 
defined by induction, though you could define an inductive type of codes to 
recurse over.

This isn't unique to type families, though, because classes are the same way: 
open, partial and defined by recursion over the structure of types; they're 
just for defining values that way, rather than types (hence why they're one of 
the ways to write outputFact above).

-- Dan