A question about constraints

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

A question about constraints

jean-christophe mincke
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
Reply | Threaded
Open this post in threaded view
|

Re: A question about constraints

Vo Minh Thu
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
Reply | Threaded
Open this post in threaded view
|

Re: A question about constraints

Bulat Ziganshin-2
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
Reply | Threaded
Open this post in threaded view
|

Re: A question about constraints

Luke Palmer-2
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
Reply | Threaded
Open this post in threaded view
|

Re: A question about constraints

Luke Palmer-2
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