Hello,
Given a type T, this type identifies a set of values and this set can be deduced from the structure of type T. i.e the type String is the set of all possible lists of character whatever their length. This being said, I have the following question: Given a type T, how is it possible to further restrict its set of values? i.e, in the above case, how is it possible to define a type String2 whose elements are any list of characters whose length is <= 5. I believe the best way to deal with that is to make String2 an ADT. This allows the constraint (in this case, the length) to be checked but hides the structure of the type, thus limits the use of pattern matching (in this case I do not want to hide the implementation of the type, so the ADT is not used that way). If one wants to use pattern matching, then the module must provide a way to convert from String2 to a type whose constructors are visible (asString in this exemple)
module A ( String2 ,mkString2 ,asString ) where import List data String2 = String2 String mkString2 l = if (length l) <= 5 then String2 l else error "length > 5" asString (String2 l) = l Btw, F# has found a nice solution to this problem, it allows the user to define an "active pattern", that is, a pattern to applies on ADT: Is there another way to address that problem in Haskell? Thank you Regards J-C Mincke _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
2008/10/2 jean-christophe mincke <[hidden email]>:
> Hello, > > Given a type T, this type identifies a set of values and this set can be > deduced from the structure of type T. > > i.e the type String is the set of all possible lists of character whatever > their length. > > This being said, I have the following question: > > Given a type T, how is it possible to further restrict its set of values? > i.e, in the above case, how is it possible to define a type String2 whose > elements are any list of characters whose length is <= 5. > > I believe the best way to deal with that is to make String2 an ADT. This > allows the constraint (in this case, the length) to be checked but hides the > structure of the type, thus limits the use of pattern matching (in this case > I do not want to hide the implementation of the type, so the ADT is not used > that way). > > If one wants to use pattern matching, then the module must provide a way to > convert from String2 to a type whose constructors are visible (asString in > this exemple) > > module A > ( > String2 > ,mkString2 > ,asString > ) > where > > import List > > data String2 = String2 String > > > mkString2 l = if (length l) <= 5 then String2 l > else error "length > 5" > > asString (String2 l) = l > > Btw, F# has found a nice solution to this problem, it allows the user to > define an "active pattern", that is, a pattern to applies on ADT: > > > http://blogs.msdn.com/dsyme/archive/2007/04/07/draft-paper-on-f-active-patterns.aspx > > Is there another way to address that problem in Haskell? I believe several proposal have been made to extend the current pattern matching mechanism. The author of the Fonctional Graph Library (FGL) has made one for instance. (Maybe see the proposals for Haskell') With the current mechanism, he uses instead a function that is applied in a case expression (thus on the right hand side of the definition). Cheers, Thu _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by jean-christophe mincke
Hello jean-christophe,
Thursday, October 2, 2008, 1:46:20 PM, you wrote: > If one wants to use pattern matching, afaik we had so-called views in early haskell versions. they proivide way to define two-way constructors - used for deconstruction via pattern-matching too views wa removed from haskell (or not included) in 1998 because they makes harder some theoretic operation, i don't remeber exactly finally, ghc now includes some form of active patterns which may be used to define your own way to decompose values. but their syntax isn't compatible with constructors so you can't define complex type which mimicks simple ones, and in particular you can replace simple type with complex one w/o rewriting all the client code imho it's serious lack in haskell support for Abstract Data Types -- Best regards, Bulat mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, Oct 2, 2008 at 4:11 AM, Bulat Ziganshin
<[hidden email]> wrote: > finally, ghc now includes some form of active patterns which may be > used to define your own way to decompose values. but their syntax > isn't compatible with constructors so you can't define complex type > which mimicks simple ones, and in particular you can replace simple > type with complex one w/o rewriting all the client code > > imho it's serious lack in haskell support for Abstract Data Types Not that this hasn't probably been discussed at length elsewhere, I wholeheartedly agree. The ability to mimic a simple type with a complex one is precisely what moves views from "syntax sugar", which does little more than to make code easier on the eyes, into a proper abstraction mechanism that actually adds engineering value. Luke _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, Oct 2, 2008 at 7:51 AM, jean-christophe mincke
<[hidden email]> wrote: > Hello, > > Thank you for your comments. > > Would not it be feasible to add constraints at type definition, something > like, in a somewhat free style syntax > > data String2 = String2 (s::String) with length s <= 5 > > and with a polymorphic type > > data List5 a= List5 (l::[a]) with length l <= 5 Well, yeah, it is possible that to a language. However, it's a question of how far you take it. What do you want that to do? Is it a runtime check on the constructor? Is it a compile-time guarantee? If it's runtime, how lazy is it -- i.e. when does it check? If it's compile-time, how do you enforce it? Basically it dumps the contents of pandora's box all over the design space, so it's easier to leave it out and just let module abstraction take care of the hard questions. There are definitely ways to simulate it: You can simulate the runtime checks as follows: subtype :: (a -> Bool) -> (a -> b) -> a -> b subtype p f x = if p x then f x else error "Subtype constraint failed" string2 :: String -> String2 string2 = subtype (\s -> length s < 5) String2 -- And don't expose String2 from the module, so string2 is the only way to make them But to give an example of why this is not a straightforward thing to answer, here's a different way which might also be correct, depending on what you want: string2 :: String -> String2 string2 s = partial 5 s where partial 0 _ = error "Subtype constraint failed" partial n [] = [] partial n (x:xs) = x:partial (n-1) xs Which lazily checks the constraint; i.e. only errors if a value is demanded beyond the index 5 and exists. Implementing Compile-time checks is typically much harder, and demands a bit more cleverness, since the way you do it is different for each type of constraint you have. For this example, you could create an algebra of lengthed lists: import Prelude hiding (++) -- Type level numbers; Z = 0, S n = n + 1. data Z data S n -- Lists of length exactly n data Listn n a where Nil :: Listn Z a Cons :: a -> Listn n a -> Listn (S n) a -- Type-level addition of numbers type family Plus m n :: * type instance Plus Z n = n type instance Plus (S m) n = S (Plus m n) -- Typed append; appends the lists, adds the lengths. -- The compiler verifies that the implementation actually does this! (++) :: Listn m a -> Listn n a -> Listn (Plus m n) a Nil ++ ys = ys Cons x xs ++ ys = Cons x (xs ++ ys) -- Type-level less than or equal; represents the type of *proofs* that m <= n. data m :<= n where LeN :: n :<= n LeS :: m :<= n -> m :<= S n -- A List5 a is a function which takes a proof than n <= 5, and returns a Listn n a type List5 a = forall n. n :<= S (S (S (S (S Z)))) -> Listn n a So that was a bit of work, wasn't it? But this solution is quite expressive; the compiler will not even compile your code if you try to construct a list with more than 5 elements. Furthermore, you can actually write most things you'd expect to because of Haskell's great GADT typechecking features :-) The downside is that you have to redefine all the standard list operations, because, well, they have different types now. The above is approaching what dependently typed languages do. My favorite is Coq (a lot of haskell folks like Agda 2), and in it you can express directly the constraint you want without all this type boilerplate: Definition List5 a := { l : List a | length l <= 5 }. But internally it is doing something very similar to the above Haskell program. This also has the property that it is impossible to write a well-typed program that constructs a List5 of length > 5. In addition, you can use all the standard list functions, however you have to prove what they do to the constraint: Theorem append_length : forall m n a (xs ys : List a), (length xs <= m) -> (length ys <= n) -> (length (xs ++ ys) <= m+n). (* prove prove prove.... *) Qed. And then you can use that theorem to prove that the parts of your program that use List5 are well-typed. Whew, so now that we're done with that, in summary, it depends on your situation how you want to do it, and there's really no "easy answer". I hope you got something out of seeing these techniques. Adding notation like that you suggest is a challenge for the language, since a runtime constraint changes the strictness properties of the object, and a compile-time constraint written that concisely actually does require full dependent types. Best to leave it to the users. Luke _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |