[Haskell-cafe] Type-Level Programming

[Brandon S Allbery KF8NH]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 6/26/10 14:58 , Jason Dagit wrote:
> On Sat, Jun 26, 2010 at 11:23 AM, Andrew Coppin <andrewcoppin at btinternet.com
> <mailto:andrewcoppin at btinternet.com>> wrote:
>     Brandon S Allbery KF8NH wrote:
>         A bit more than that:  imagine now that you can (a) replace that 7
>         with a
>         variable and (b) do math on it in a type declaration.
>
>     So is there a specific reason why Haskell isn't dependently typed then?
>
> Or you could ask, So is there a specific reason why C isn't a functional
> language?

More to the point, Haskell was a bit too frozen in stone when dependent type
theory reached the point of being implementable.  As a case in point, you'll
notice in my sized-list example in pseudo-Haskell I had to drag in syntax
from ML to distinguish type variables from value variables?  Hard to escape
that with Haskell as it currently exists --- but in a proper dependently
typed system, there is no such distinction:  types aren't different kinds of
things from values.  (Or in the usual lingo, types are first class values in
dependently-typed languages.)  Compare my example to the Agda example
someone else posted; Agda is a proper dependently typed language, and the
value and type variables are treated exactly the same way.

- -- 
brandon s. allbery     [linux,solaris,freebsd,perl]      allbery at kf8nh.com
system administrator  [openafs,heimdal,too many hats]  allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university      KF8NH
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkwmcEgACgkQIn7hlCsL25UaRgCgybBPBhtn2evzDA6+0D9L3uph
XVsAni86B2NDPZPCPvIc1Us53rj3hh06
=LxLd
-----END PGP SIGNATURE-----