Re: [Haskell-cafe] linear and dependent types
On Saturday 19 February 2011 1:11:23 AM Vasili I. Galchin wrote: > BTW I was thinking of http://www.ats.org when I asked this question. Technically speaking, if one considers ATS to be dependently typed, then one might as well also consider GHC to be dependently typed (with the right extensions enabled). ATS would easily be a nicer language in that respect, though. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear and dependent types
There has been extensive discussion of whether Haskell has dependent types, made larger by the fact that the definition of dependently-typed languages is a bit fuzzy. On some accounts, type functions or GADTs are sufficient for calling a language dependently-typed, and Haskell got both features. The situation is clearer with linear types. First of all, Haskell has all facilities for statically ensuring the proper use of resources. The simplest example is enforcing the locking protocol: a lock can be acquired no more than once; only acquired locks may be released, all acquired locks must be released at the end. This simple example is described in Sec 5.2 of http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf That example can be made more complex: a program with two locks choosing the lock to acquire based on the data it reads from a file. We can still statically guarantee that all acquired locks are released and no lock is acquired or released twice -- even if we cannot statically tell which particular lock will be acquired during a program run. Other examples of resource control include session types and regions. There are several Hackage packages with these keywords. Generally, Haskell can easily embed languages with dependent or linear types -- just as easily as Haskell embeds languages with IO, global mutable state, non-determinism. The latter languages go by the name of monads. One can easily embed typed linear lambda-calculus, with Haskell type-checker ensuring that each bound variable is referenced exactly once. http://okmij.org/ftp/tagless-final/course/index.html#linear The linear lambda-calculus turns out not very useful; no wonder Girard had to add exponentials. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear and dependent types
Thanks Bas. BTW I was thinking of http://www.ats.org when I asked this question. REgards, Vasili On Fri, Feb 18, 2011 at 6:19 PM, Bas van Dijk wrote: > On 18 February 2011 20:04, Vasili I. Galchin wrote: > >Does Haskell currently have support for linear types and dependent > > types? If so, is it necessary to specify a "pragma" to use and if so, > what > > is the pragma(s)? > > While Haskell doesn't have full dependent types, as found in say Agda, > it (or rather GHC) does have some extensions that allow you to get > many of the advantages of full dependent types. > > You may want to check out the documentation of: multi parameter type > classes, functional dependencies, type families, higher ranked types, > generalized algebraic datatypes, scoped type variables, pfff... we > have so many toys! :-) > > You may also want to read some of the papers mentioned in: > > > http://www.haskell.org/haskellwiki/Dependent_type#Dependent_types_in_Haskell_programming > > Regards, > > Bas > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear and dependent types
On 18 February 2011 20:04, Vasili I. Galchin wrote: > Does Haskell currently have support for linear types and dependent > types? If so, is it necessary to specify a "pragma" to use and if so, what > is the pragma(s)? While Haskell doesn't have full dependent types, as found in say Agda, it (or rather GHC) does have some extensions that allow you to get many of the advantages of full dependent types. You may want to check out the documentation of: multi parameter type classes, functional dependencies, type families, higher ranked types, generalized algebraic datatypes, scoped type variables, pfff... we have so many toys! :-) You may also want to read some of the papers mentioned in: http://www.haskell.org/haskellwiki/Dependent_type#Dependent_types_in_Haskell_programming Regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear and dependent types
vigalchin: >Hello, > >�� Does Haskell currently have support for linear types and dependent > types? No. -- Don P.S. :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] linear and dependent types
Hello, Does Haskell currently have support for linear types and dependent types? If so, is it necessary to specify a "pragma" to use and if so, what is the pragma(s)? Kind regards, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
