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

J. Garrett Morris jgmorris at cs.pdx.edu
Thu Jun 10 15:56:23 EDT 2010


On Thu, Jun 10, 2010 at 11:00 AM, Norman Ramsey <nr at cs.tufts.edu> 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.

This is not new with type families; exactly the same sort of type can
be achieved with functional dependencies.  For instance:

class F t u | t -> u    -- requires that 'u' be functionally dependent on 't'

instance F Int Bool
instance F Bool Char

foo :: F t u => t -> u
foo = ...

In this case, the type of foo cannot range freely in both t and u;
while Int -> Bool is a valid typing, Int -> Char is not.  It might
seem that this case is not as tricky, since there is an explicit
qualifier limiting the type of foo.  However, the differences between
this version and the version with type families are purely syntactic.
There have been various suggestions for allowing classes with
functional dependencies to be written as functions, which would allow
the declaration of foo to be written:

foo :: t -> F t

Perhaps doing the reverse would help to explain the type in your
message?  If instead of writing

outputFact :: a -> Info a

we wrote

outputFact :: b ~ Info a => a -> b

then it looks more like a "conventional" qualified type.

 /g


More information about the Types-list mailing list