
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

On 18 February 2011 20:04, Vasili I. Galchin
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... Regards, Bas

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
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...
Regards,
Bas

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
participants (4)
-
Bas van Dijk
-
Dan Doel
-
Don Stewart
-
Vasili I. Galchin