CODEWITHSUNDEEP
haskelltype-constraints
user3680029
user3680029

Reputation: 179

Haskell Type Level Constraint

I'm curious if it's possible to write something like this (pseudo code) in Haskell:

data Clock = Clock {hour :: (0 <= Int <= 24),  minutes :: (0 <= Int <= 60)}

to make impossible (at the type level) to create something like this:

let a = Clock 34 236

Or should one use a kind of Clock builder which will check and create a valid Clock time?

Upvotes: 1

Views: 276

Answers (2)

Noughtmare
Noughtmare

Reputation: 10695

Smart constructors

One simple way to do this is to use smart encapsulation and smart constructors:

module HoursAndMinutes (Hours, mkHours, getHours, Minutes, mkMinutes, getMinutes) where

newtype Hours = UnsafeHours Int

mkHours :: Int -> Maybe Hours
mkHours n | 0 <= n && n < 24 = Just (UnsafeHours n)
          | otherwise = Nothing

getHours :: Hours -> Int
getHours (UnsafeHours n) = n

newtype Minutes = UnsafeMinutes Int

mkMinutes :: Int -> Maybe Minutes
mkMinutes n | 0 <= n && n < 60 = Just (UnsafeMinutes n)
            | otherwise = Nothing

getMinutes :: Minutes -> Int
getMinutes (UnsafeMinutes n) = n

Now in your other code if you import HoursAndMinutes then you cannot construct invalid Hours or Minutes.

data Clock = Clock {hours :: Hours,  minutes :: Minutes}

Then this will result in Nothing:

Clock <$> mkHours 34 <*> mkMinutes 236

Refined

You can use the built-in predicates from refined package to simplify this approach slightly:

data Clock = Clock
  { hours   :: Refined (FromTo 0 23) Int
  , minutes :: Refined (FromTo 0 59) Int
  }

Then you can construct one with:

Clock <$> refine 34 <*> refine 236

Which will be Left (RefineSomeException ...).

The disadvantage is still that the checks are at runtime. You can get compile time checks by using Template Haskell:

Clock $$(refineTH 34) $$(refineTH 236)

This will throw an exception at compile time.

Liquid Haskell

You can make this more convenient by using Liquid Haskell as Willem van Onsem suggests in his comment:

module Clock where

data Clock = Clock { hours :: Int, minutes :: Int } deriving Show
{-@ data Clock = Clock
      { hours   :: {h:Int | 0 <= h && h < 24}
      , minutes :: {m:Int | 0 <= m && m < 60}
      } @-}

goodClock :: Clock
goodClock = Clock 16 49

badClock :: Clock
badClock = Clock 34 236 -- this gives an error

Try it out here.

Upvotes: 7

leftaroundabout
leftaroundabout

Reputation: 120751

The concrete example is best expressed with types from the modular-arithmetic package:

{-# LANGUAGE TypeOperators, TypeFamilies, DataKinds #-}

import Data.Modular

data Clock = Clock {hour :: Int/24,  minutes :: Int/60}

Note that the upper bounds are exclusive here, as you should have probably had in your code as well.

Modular arithmetic is a special case of a quotient type, which is in some ways more practical than constrained types. But Haskell has no general, direct support for either. As Willem Van Onsen mentioned, Liquid Haskell adds such functionality. Can't say much about that, but I've heard multiple times that it works surprisingly well.

Upvotes: 7

Related Questions