How to make a type with restrictions

Question

For example I want to make a type MyType of integer triples. But not just Cartesian product of three Integer, I want the type to represent all (x, y, z) such that x + y + z = 5.

How do I do that? Except of using just (x, y) since z = 5 - x - y.

And the same question if I have three constructors A, B, C and the type should be all (A x, B y, C z) such that x + y + z = 5.

Answer 1

I think the trick here is that you don't enforce it on the type-level, you use "smart constructors": i.e. only allow creation of such "tuples" via a function that generates such values:

module Test(MyType,x,y,z,createMyType) where

data MyType = MT { x :: Int, y :: Int, z :: Int }

createMyType :: Int -> Int -> MyType
createMyType myX myY = MT { x = myX, y = myY, z = 5 - myX - myY }

If you want to generate all possible such values, then you can write a function to do so, either with provided or specified bounds.

It may very well be possible to use type-level Church Numerals or some such so as to enforce creation of these, but it's almost definitely too much work for what you probably want/need.

This might not be what you want (i.e. "Except of using just (x, y) since z = 5 - x - y") but it makes more sense than trying to have some kind of enforced restriction on the type level for allowing valid values.

Types can ensure the correct "type" of value (no pun intended); to ensure validity of values you hide the constructor and only allow creation via approved functions that guarantee any invariants you require.

Answer 2

Yes, smart constructors or Agda are the way to go here, but if you really wanted to go crazy with the "dependent" approach, in Haskell:

{-# LANGUAGE GADTs, TypeFamilies, RankNTypes, StandaloneDeriving, UndecidableInstances, TypeOperators #-}

data Z = Z
data S n = S n

data Nat n where
  Zero :: Nat Z
  Suc  :: Nat n -> Nat (S n)

deriving instance Show (Nat n)

type family (:+) a b :: *
type instance (:+) Z b = b
type instance (:+) (S a) b = S (a :+ b)

plus :: Nat x -> Nat y -> Nat (x :+ y)
plus Zero y = y
plus (Suc x) y = Suc (x `plus` y)

type family (:*) a b :: *
type instance (:*) Z b = Z
type instance (:*) (S a) b = b :+ (a :* b)

times :: Nat x -> Nat y -> Nat (x :* y)
times Zero y = Zero
times (Suc x) y = y `plus` (x `times` y)

data (:==) a b where
  Refl :: a :== a

deriving instance Show (a :== b)

cong :: a :== b -> f a :== f b
cong Refl = Refl

data Triple where
  Triple :: Nat x -> Nat y -> Nat z -> (z :== (x :+ y)) -> Triple

deriving instance Show Triple

-- Half a decision procedure
equal :: Nat x -> Nat y -> Maybe (x :== y)
equal Zero Zero = Just Refl
equal (Suc x) Zero = Nothing
equal Zero (Suc y) = Nothing
equal (Suc x) (Suc y) = cong `fmap` equal x y

triple' :: Nat x -> Nat y -> Nat z -> Maybe Triple
triple' x y z = fmap (Triple x y z) $ equal z (x `plus` y)

toNat :: (forall n. Nat n -> r) -> Integer -> r
toNat f n | n < 0 = error "why can't we have a natural type?"
toNat f 0 = f Zero
toNat f n = toNat (f . Suc) (n - 1)

triple :: Integer -> Integer -> Integer -> Maybe Triple
triple x y z = toNat (\x' -> toNat (\y' -> toNat (\z' -> triple' x' y' z') z) y) x

data Yatima where
  Yatima :: Nat x -> Nat y -> Nat z -> ((x :* x) :+ (y :* y) :+ (z :* z) :== S (S (S (S (S Z))))) -> Yatima

deriving instance Show Yatima

yatima' :: Nat x -> Nat y -> Nat z -> Maybe Yatima
yatima' x y z = 
  fmap (Yatima x y z) $ equal ((x `times` x) `plus` (y `times` y) `plus` (z `times` z)) (Suc (Suc (Suc (Suc (Suc Zero)))))

yatima :: Integer -> Integer -> Integer -> Maybe Yatima
yatima x y z = toNat (\x' -> toNat (\y' -> toNat (\z' -> yatima' x' y' z') z) y) x


{-
λ> triple 3 4 5
Nothing
λ> triple 3 4 7
Just (Triple (Suc (Suc (Suc Zero))) (Suc (Suc (Suc (Suc Zero)))) Refl (Suc (Suc (Suc (Suc (Suc (Suc (Suc Zero))))))))

λ> yatima 0 1 2 
Just (Yatima Zero (Suc Zero) (Suc (Suc Zero)) Refl)
λ> yatima 1 1 2 
Nothing
-}

And bam, you have a statically checked invariant in your code! Except you can lie...

Answer 3

The normal dependently-typed way to do this would be to use a sigma (dependent product) type, for example in Agda:

open import Relation.Binary.PropositionalEquality (_≡_)
open import Data.Nat (ℕ; _+_)
open import Data.Product (Σ; ×; _,_)

FiveTriple : Set
FiveTriple = Σ (ℕ × ℕ × ℕ) (λ{ (x , y , z) → x + y + z ≡ 5 })

someFiveTriple : FiveTriple
someFiveTriple = (0 , 2 , 5) , refl

This is why Σ is often called an ‘existential’ type: it allows you to specify both some data and some property about that data.

Answer 4

I'm not an expert on this, but I don't think you can implement this in Haskell at the type level, as Haskell does not support dependent types. You might want to look at Agda.