VerifiedSmartConstructor.idr

module Main

||| The smart consturctor tool:
||| Check whether an element belongs to a given subset
subset : ((x: a) -> Dec (prop x)) -> a -> Either a (Subset a prop)
subset dec y with (dec y)
  | (Yes prf) = pure (Element y prf)
  | (No contra) = Left y

-- Example

-- Given a simple type Person
record Person where
  constructor MkPerson
  name : String
  age : Nat


-- We want to be able to build a subtype of Person, for adults (18+)
Adult : Nat -> Type
Adult k = Subset Person (LTE k . age)

-- Here is the smart constructor, providing a person, either we can prove that they are more than 18,
-- and we have an Adult, or we can't and we cannot build an Adult value.
adult : Person -> Either Person (Adult 18)
adult = subset (\x => isLTE 18 $ age x)

-- The main difference with another language is that I do not need to hide the
-- Adult consturctor to ensure that my values are correct.

testAdult : Either Person (Adult 18)
testAdult = adult $ MkPerson "me" 38 -- It's a Right (and it's verbose, as I'm a bit old now)

testChild : Either Person (Adult 18)
testChild = adult $ MkPerson "myDaughter" 0 -- Lovely girl, it's a Left.