To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 30/11/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                        Vendredi 30 novembre, 10h30

                             ------------------
                             Simon Peyton Jones
                             ------------------

                             Microsoft Research

                     =================================
                     Indexed type families for Haskell
                     =================================

A number of strands in type-system design have been coming together: GADTs,
type-indexed representations, computation at the type level, and functional
dependencies. All involve extra sophistication in reasoning about type
equality. This is not a merely theoretical exercise: we need this stuff to
express vectorised programs in the Nested Data Parallel Haskell project.

Thus motivated, we have been developing some general source-language
constructs for writing programs involving type equality, a type inference
algorithm for type-checking such programs, and a strongly-typed intermediate
language into which these programs can be elaborated.

In this talk I will try to give a flavour of what we have done and what we are
working on. It is very much work in progress; we are still exploring the
design space.

This is joint work with Manuel Chakravarty, Tom Schrijvers, Martin Sulzmann.