Re: [Haskell-cafe] Type-Level Programming

-----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 mailto:andrewcoppin@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@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@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-----