Re: Another typing question
On Tuesday 05 August 2003 15:23, Wolfgang Jeltsch wrote: There probably are ways to achieve this with Haskell's type system. The exact solution depends on what exactly you want. For just distinguishing between lists of different lengths you could use tuples like (a,a) (list of length 2) (a,a,a) (list of length 3) etc. What would be the advantage to using standard lists? In both cases I'd need explicit length checks everywhere. A better solution might be: data EmptyList element = EmptyList data TrueList list element = TrueList element (list element) A list of four Ints for example would be represented by a value of type TrueList (TrueList (TrueList (TrueList EmptyList))) Int. Isn't that just the Haskell list type by another name? You could define different types for different natural numbers: data Zero = Zero data Succ number = Succ number and do simple arithmetic with them at the type level: class Sum a b c | (a, b) - c instance Sum 0 a a instance Sum a b c = Sum (Succ a) b (Succ c) That looks interesting, I need to look into multiple parameter classes... At the moment, I cannot think of a way of defining a list type which is parameterized by such natural types. What I mean is having a type List :: * - * - * where for our above example of a list of four Ints we would have the type List (Succ (Succ (Succ (Succ Zero Int That's what I would like... What I can think of, is an association between our above list types (EmptyList and TrueList) and our natural number types by a multi-parameter class: class HasLength list length | list - length instance HasLength EmptyList Zero instance HasLength list length = HasLength (TrueList list) (Succ length) Again those multi-parameter classes... and off I go to the Haskell Web site ;-) Thanks for your comments! Konrad. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Tuesday, 2003-08-05, 15:22, CEST, Nick Name wrote: [...] Is there any way to parametrize a type by a value, rather than another type? What I would like to do is to define list of length 3 and list of length 4 as separate parametrization of the same type, such that I could write functions that accept lists (under my new typename) of any length as long as parameters have the same length. The goal is to remove the need for runtime checks all over the code. This is called dependent types and is not a feature of haskell (nor of any language that I know); there was cayenne (try a google search) but I don't believe it is still mantained. Well, there are, e.g., Ada and C++ which allow types to be parametrized by values. The point is that they obviously still use runtime checks, it's just that you don't have to code these checks explicitely. BTW, why is there no general interest for such a thing as dependent types? What negative consequences does their implementation have? I think, sometimes they could be quite handy. V. W. ;-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Tuesday, 2003-08-05, 15:22, CEST, Nick Name wrote: snip This is called dependent types and is not a feature of haskell (nor of any language that I know); there was cayenne (try a google search) but I don't believe it is still mantained. snip BTW, why is there no general interest for such a thing as dependent types? What negative consequences does their implementation have? It depends on whether you just want to write functions to take in values of such types, or whether you want to write functions to return values of such types. Doing the former uses dependant products, which would require a significant extension to GHC's guts, but not (AIUI) inherently unpleasant. Doing the latter (AIUI) essentially requires dependant sums. Basically, a family of types A_i parameterized by a value i :: I is written, for long-honored traditional reasons too complex to get into here, Sigma i::I.A_i. Now, if you have such dependant sums, there's a bad interaction with polymorphism: either you must have a type alpha which cannot appear in a family of types A_i in a dependant sum, or, for any function f :: alpha - alpha, there exists a type beta such that f cannot be aplied at either beta or Sigma i::Int.beta. Clear? The alternative, btw., is to have both dependant sums and an undecidable type-checking problem. I think, sometimes they could be quite handy. Sure. Sarcastic comment censored. Jon Cast ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
I wrote: Wolfgang Jeltsch [EMAIL PROTECTED] wrote: On Tuesday, 2003-08-05, 15:22, CEST, Nick Name wrote: snip This is called dependent types and is not a feature of haskell (nor of any language that I know); there was cayenne (try a google search) but I don't believe it is still mantained. snip BTW, why is there no general interest for such a thing as dependent types? What negative consequences does their implementation have? It depends on whether you just want to write functions to take in values of such types, or whether you want to write functions to return values of such types. Doing the former uses dependant products, which would require a significant extension to GHC's guts, but not (AIUI) inherently unpleasant. Doing the latter (AIUI) essentially requires dependant sums. Basically, a family of types A_i parameterized by a value i :: I is written, for long-honored traditional reasons too complex to get into here, Sigma i::I.A_i. Now, if you have such dependant sums, there's a bad interaction with polymorphism: either you must have a type alpha which cannot appear in a family of types A_i in a dependant sum, or, for any function f :: alpha - alpha, there exists a type beta such that f cannot be aplied at either beta or Sigma i::Int.beta. Clear? Actually, on second thought, I think this could be simplified to: if we have dependant types, then either there is a type which cannot be used in a dependant type, or for every polymorphic function there is a type it cannot be applied at. Jon Cast ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Another typing question
Is there any way to parametrize a type by a value, rather than another type? What I would like to do is to define list of length 3 and list of length 4 as separate parametrization of the same type, such that I could write functions that accept lists (under my new typename) of any length as long as parameters have the same length. The goal is to remove the need for runtime checks all over the code. Konrad. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Tue, 5 Aug 2003 15:30:44 +0200 Wolfgang Jeltsch [EMAIL PROTECTED] wrote: What negative consequences does their implementation have? I think, sometimes they could be quite handy. That you have to solve a constraint system to compile your program, AFAIK. But I guess that a brave GHC user should not be afraid of waiting at compile-time ^_^ V. -- Teatri vuoti e inutili potrebbero affollarsi se tu ti proponessi di recitare te [CCCP] ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
Samuel E Moelius, wrote (on Wed, 06 Aug 2003 at 15:35): On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote: This is why most sensible dependent type theories have a hierarchy of universes behind the scenes. You can think of * in Haskell as the lowest universe, inhabited by types. Why wouldn't terms be the lowest universe? A universe is a type of types/set-like-things, modulo a pile of subtleties. (The first of which is that it is actually a type of codes for types.) I think the term universe, which afaik was introduced into type theory by Martin-Lof, was chosen for its use in the foundations of category theory in dealing with questions of size (smallness/largeness). Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote: This is why most sensible dependent type theories have a hierarchy of universes behind the scenes. You can think of * in Haskell as the lowest universe, inhabited by types. Why wouldn't terms be the lowest universe? Sam Moelius ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Tue, 5 Aug 2003 12:23:06 +0200 Konrad Hinsen [EMAIL PROTECTED] wrote: 3 Is there any way to parametrize a type by a value, rather than another type? What I would like to do is to define list of length 3 and list of length 4 as separate parametrization of the same type, such that I could write functions that accept lists (under my new typename) of any length as long as parameters have the same length. The goal is to remove the need for runtime checks all over the code. This is called dependent types and is not a feature of haskell (nor of any language that I know); there was cayenne (try a google search) but I don't believe it is still mantained. BTW, why is there no general interest for such a thing as dependent types? V. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
A better solution might be: data EmptyList element = EmptyList data TrueList list element = TrueList element (list element) A list of four Ints for example would be represented by a value of type TrueList (TrueList (TrueList (TrueList EmptyList))) Int. Isn't that just the Haskell list type by another name? I think it's quite different. A Haskell list looks like this: 1 : 2 : 3 : 4 : []:: [Int] Note that the type gives no indication of the length of the list. Wolfgang's lists look like this (I'm adding a 'T_' prefix to the names of the type constructors to remove some ambiguity) 1 `TrueList` 2 `TrueList` 3 `TrueList` 4 `TrueList` EmptyList :: T_TrueList (T_TrueList (T_TrueList (T_TrueList T_EmptyList))) Int Note that you can determine the length of the list from the _type_ by counting the occurences of T_TrueList in the type. You can see a fully worked use of this approach in Mark Jones' paper about typechecking Java bytecodes by translating them into a Haskell program using this kind of encoding. (I'm not sure if Mark would characterise the paper this way but it's what I remember him doing...) http://www.cse.ogi.edu/~mpj/pubs/funJava.html -- Alastair Reid ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
Is there any way to parametrize a type by a value, rather than another type? I believe the following web page answers your question: http://pobox.com/~oleg/ftp/Haskell/number-parameterized-types.html It uses parameterization by decimal numbers -- which seem more natural to read. It would be interesting to know if/how you could, e.g., define a concatenation function with a type like Yes, you can -- and the page referenced above does that. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
On Tue, 5 Aug 2003 15:23:09 +0200 Wolfgang Jeltsch [EMAIL PROTECTED] wrote: You could define different types for different natural numbers: data Zero = Zero data Succ number = Succ number This resembles http://www.brics.dk/RS/01/10/ V. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
