Check constructor's field numeric value at compile time

Dmitriy Matrosov

2 Sep 2014 2 Sep '14

7:32 p.m.

Hi. I have a type data Interval = Seconds Float | MicroSeconds Int The Float field of data constructor Seconds should be >= 1, and Int field of constructor MicroSeconds should be in the range from 0 to 1000000. How can i write this constraints so they're checked at compile time, not at runtime? -- Dmitriy Matrosov

Show replies by date

Alexandre Lucchesi

2 Sep 2 Sep

8:58 p.m.

New subject: Check constructor's field numeric value at compile time

You can't do that within the data type declaration. In order to add such constraints you should define "constructor functions" and apply the validation there, i.e.: newSecondsInterval :: Float -> Maybe Interval newSecondsInterval n | n >= 1 = Just $ Seconds n | otherwise = Nothing Note that the "Maybe" type is only a way to handle the case where the supplied value is invalid. Also, in order to provide encapsulation and ensure no one is going to create a new "Interval" by using "Seconds" and "MicroSeconds", you should hide these value constructors in the export list of your module. On Tue, Sep 2, 2014 at 4:32 PM, Dmitriy Matrosov wrote:

...

Hi.

I have a type

data Interval = Seconds Float | MicroSeconds Int

The Float field of data constructor Seconds should be >= 1, and Int field of constructor MicroSeconds should be in the range from 0 to 1000000.

How can i write this constraints so they're checked at compile time, not at runtime?

-- Dmitriy Matrosov _______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

-- alexandre lucchesi *Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away!*

Julian Birch

10:02 p.m.

New subject: Check constructor's field numeric value at compile time

Also, if you want your mind blown, check out Idris. On Tuesday, September 2, 2014, Alexandre Lucchesi < alexandrelucchesi@gmail.com> wrote:

...

You can't do that within the data type declaration.

In order to add such constraints you should define "constructor functions" and apply the validation there, i.e.:

newSecondsInterval :: Float -> Maybe Interval newSecondsInterval n | n >= 1 = Just $ Seconds n | otherwise = Nothing

Note that the "Maybe" type is only a way to handle the case where the supplied value is invalid. Also, in order to provide encapsulation and ensure no one is going to create a new "Interval" by using "Seconds" and "MicroSeconds", you should hide these value constructors in the export list of your module.

On Tue, Sep 2, 2014 at 4:32 PM, Dmitriy Matrosov javascript:_e(%7B%7D,'cvml','sgf.dma@gmail.com');> wrote:

...
Hi.

I have a type

data Interval = Seconds Float | MicroSeconds Int

The Float field of data constructor Seconds should be >= 1, and Int field of constructor MicroSeconds should be in the range from 0 to 1000000.

How can i write this constraints so they're checked at compile time, not at runtime?

-- Dmitriy Matrosov _______________________________________________ Beginners mailing list Beginners@haskell.org javascript:_e(%7B%7D,'cvml','Beginners@haskell.org'); http://www.haskell.org/mailman/listinfo/beginners

-- alexandre lucchesi

*Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away!*

-- Sent from an iPhone, please excuse brevity and typos.

Kim-Ee Yeoh

3 Sep 3 Sep

3:04 a.m.

New subject: Check constructor's field numeric value at compile time

On Wed, Sep 3, 2014 at 3:58 AM, Alexandre Lucchesi < alexandrelucchesi@gmail.com> wrote:

...

In order to add such constraints you should define "constructor functions" and apply the validation there, i.e.:

To OP: Yes, the searchable term is "smart constructors". However, it has been used at least once on this list to mean something different, so look out. -- Kim-Ee

Alexandre Lucchesi

3:07 a.m.

New subject: Check constructor's field numeric value at compile time

Hmm.. Nice to know about that! Thank you. :) On Wed, Sep 3, 2014 at 12:04 AM, Kim-Ee Yeoh wrote:

...

On Wed, Sep 3, 2014 at 3:58 AM, Alexandre Lucchesi < alexandrelucchesi@gmail.com> wrote:

...
In order to add such constraints you should define "constructor functions" and apply the validation there, i.e.:

To OP: Yes, the searchable term is "smart constructors". However, it has been used at least once on this list to mean something different, so look out.

-- Kim-Ee

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

-- alexandre lucchesi *Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away!*

Brandon Allbery

3:07 a.m.

New subject: Check constructor's field numeric value at compile time

On Tue, Sep 2, 2014 at 11:04 PM, Kim-Ee Yeoh wrote:

...

On Wed, Sep 3, 2014 at 3:58 AM, Alexandre Lucchesi < alexandrelucchesi@gmail.com> wrote:

...
In order to add such constraints you should define "constructor functions" and apply the validation there, i.e.:

To OP: Yes, the searchable term is "smart constructors". However, it has been used at least once on this list to mean something different, so look out.

Also note that this will not actually check at compile time; to do that you need type level stuff that ghc is still finding its way through. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Kim-Ee Yeoh

3:07 a.m.

New subject: Check constructor's field numeric value at compile time

On Wed, Sep 3, 2014 at 2:32 AM, Dmitriy Matrosov wrote:

...

How can i write this constraints so they're checked at compile time, not at runtime?

Smart constructors won't check them at compile time but it does the next best thing, which is validate at the earliest possible moment. -- Kim-Ee

David Virebayre

8 Sep 8 Sep

2:31 p.m.

New subject: Check constructor's field numeric value at compile time

2014-09-03 5:07 GMT+02:00 Kim-Ee Yeoh :

...

On Wed, Sep 3, 2014 at 2:32 AM, Dmitriy Matrosov wrote:

...
How can i write this constraints so they're checked at compile time, not at runtime?

Smart constructors won't check them at compile time but it does the next best thing, which is validate at the earliest possible moment.

In between compile time and runtime, you probably could use refinements types; see LiquidHaskell (http://goto.ucsd.edu:8090/index.html, https://github.com/ucsd-progsys/liquidhaskell/ ) David.

4058

Age (days ago)

4064

Last active (days ago)

List overview

Download

7 comments

6 participants

participants (6)

Alexandre Lucchesi
Brandon Allbery
David Virebayre
Dmitriy Matrosov
Julian Birch
Kim-Ee Yeoh