[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Dan Doel
dan.doel at gmail.com
Sat Mar 14 10:26:47 EDT 2009
On Saturday 14 March 2009 8:12:09 am Conor McBride wrote:
> Rome wasn't burnt in a day.
>
> Of course I want more than just numerical indexing (and I even
> have a plan) but numeric constraints are so useful and have
> so much of their own peculiar structure that they're worth
> studying in their own right, even for languages which do have
> full dependent types, let alone Haskell. We'll carry out this
> project with an eye to the future, to make sure it's compatible
> with full dependent types.
One should note that ATS, which has recently been generating some excitement,
doesn't have "full" dependent types, depending on what exactly you mean by
that. For instance, it's dependent typing for integers consist of:
1) A simply typed static/type-level integer type
2) A family of singleton types int(n) parameterized by the static type.
For instance, int(5) is the type that contains only the run-time value 5.
3) An existential around the above family for representing arbitrary
integers.
where, presumably, inspecting a value of the singleton family informs the type
system in some way. But, we can already do this in GHC (I'll do naturals):
-- datakind nat = Z | S nat
data Z
data S n
-- family linking static and dynamic
data NatFam :: * -> * where
Z :: NatFam Z
S :: NatFam n -> NatFam (S n)
-- existential wrapper
data Nat where
N :: forall n. NatFam n -> Nat
Of course, ATS' are built-in, and faster, and the type-level programming is
probably easier, but as far as dependent typing goes, GHC is already close (I
don't think you'd ever see the above scheme in something like Agda or Coq with
'real' dependent types).
And this isn't just limited to integers. If you go look at the quicksort
example, you'll see something that when translated to GHC looks like:
-- datakind natlist = nil | cons nat natlist
data Nil
data n ::: l
data ListFam :: * -> * where
Nil :: ListFam Nil
(:::) :: forall n l. NatFam n -> ListFam l -> ListFam (n ::: l)
data List where
L :: forall l. ListFam l -> List
So this sort of type-level vs. value-level duplication with GADTs tying the
two together seems to be what is always done in ATS. This may not be as sexy
as taking the plunge all the way into dependent typing ala Agda and Coq, but
it might be a practical point in the design space that GHC/Haskell-of-the-
future could move toward without too much shaking up. And if ATS is any
indication, it allows for very efficient code, to boot. :)
Cheers,
-- Dan
More information about the Haskell-Cafe
mailing list