Add basic support for exceptions

lib/base/Haskell/Control/Exception.agda

@@ -1,11 +1,146 @@
 module Haskell.Control.Exception where
 
 open import Haskell.Prim
+open import Haskell.Prim.Either
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Monad
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Show
+open import Haskell.Prim.String
 
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 
-assert : (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
+private variable
+  e1 e2 : Set
+
+record Exception (e : Set) : Set where
+  no-eta-equality
+  field
+    overlap {{iShow}} : Show e
+    displayException : e → String
+open Exception {{...}} public
+
+{-# COMPILE AGDA2HS Exception existing-class #-}
+
+postulate
+  IOException : Set
+  instance
+    iEqIOException : Eq IOException
+    iExceptionIOException : Exception IOException
+
+data ArithException : Set where
+  Overflow UnderFlow LossOfPrecision DivideByZero Denormal : ArithException
+  RatioZeroDenominator : ArithException
+
+postulate instance
+  iOrdArithException : Ord ArithException
+  iExceptionArithException : Exception ArithException
+
+data ArrayException : Set where
+  IndexOutOfBounds UndefinedElement : String → ArrayException
+
+postulate instance
+  iOrdArrayException : Ord ArrayException
+  iExceptionArrayException : Exception ArrayException
+
+record AssertionFailed : Set where
+  no-eta-equality; pattern
+  field theFailedAssertion : String
+
+postulate instance
+  iExceptionAssertionFailed : Exception AssertionFailed
+
+record NoMethodError : Set where
+  no-eta-equality; pattern
+  field theNoMethodError : String
+
+postulate instance
+  iExceptionNoMethodError : Exception NoMethodError
+
+record PatternMatchFail : Set where
+  no-eta-equality; pattern
+  field thePatternMatchFail : String
+
+postulate instance
+  iExceptionPatternMatchFail : Exception PatternMatchFail
+
+record RecConError : Set where
+  no-eta-equality; pattern
+  field theRecConError : String
+
+postulate instance
+  iExceptionRecConError : Exception RecConError
+
+record RecSelError : Set where
+  no-eta-equality; pattern
+  field theRecSelError : String
+
+postulate instance
+  iExceptionRecSelError : Exception RecSelError
+
+record RecUpdError : Set where
+  no-eta-equality; pattern
+  field theRecUpdError : String
+
+postulate instance
+  iExceptionRecUpdError : Exception RecUpdError
+
+record ErrorCall : Set where
+  no-eta-equality; pattern
+  field theErrorCall : String
+
+postulate instance
+  iOrdErrorCall : Ord ErrorCall
+  iExceptionErrorCall : Exception ErrorCall
+
+record TypeError : Set where
+  no-eta-equality; pattern
+  field theTypeError : String
+
+postulate instance
+  iExceptionTypeError : Exception TypeError
+
+postulate
+  @0 MayThrow : Set → Set
+
+  throw : {{Exception e}} → @0 {{MayThrow e}} → e → a
+  throwIO : {{Exception e}} → @0 {{MayThrow e}} → e → IO a
+
+postulate
+  catch : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → (e → IO a) → IO a
+  catchJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → (b → IO a) → IO a
+
+handle : {{Exception e}} → (e → IO a) → (@0 {{MayThrow e}} → IO a) → IO a
+handle = flip catch
+
+handleJust : {{Exception e}} → (e → Maybe b) → (b → IO a) → (@0 {{MayThrow e}} → IO a) → IO a
+handleJust f = flip (catchJust f)
+
+try : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → IO (Either e a)
+try a = catch (fmap Right a) (return ∘ Left)
+
+tryJust : {{Exception e}} → (e → Maybe b) → (@0 {{MayThrow e}} → IO a) → IO (Either b a)
+tryJust p a = catchJust p (fmap Right a) (return ∘ Left)
+
+postulate
+  evaluate : a → IO a
+  mapException : {{Exception e1}} → {{Exception e2}} → (e1 → e2) → a → a
+
+assert : @0 {{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
-assert _ {{False ⟨ _ ⟩}} x = oops
-  where postulate oops : _
+assert _ {{False ⟨ _ ⟩}} x = throw oops
+  where postulate oops : AssertionFailed
+
+postulate
+  bracket : IO a → (a → IO b) → (a → IO c) → IO c
+  bracket_ : IO a → IO b → IO c → IO c
+  bracketOnError : IO a → (a → IO b) → (a → IO c) → IO c
+  finally : IO a → IO b → IO a
+  onException : IO a → IO b → IO a
+
+ioException : @0 {{MayThrow IOException}} → IOException → IO a
+ioException = throwIO

lib/base/Haskell/Extra/Dec.agda

@@ -1,11 +1,14 @@
 module Haskell.Extra.Dec where
 
-open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
 open import Haskell.Extra.Refinement
+
 open import Agda.Primitive
 
 private variable
-  ℓ : Level
   P : Type
 
 @0 Reflects : Type ℓ → Bool → Type ℓ

lib/base/Haskell/Extra/Refinement.agda

@@ -1,10 +1,7 @@
 module Haskell.Extra.Refinement where
 
-open import Haskell.Prelude
-open import Agda.Primitive
-
-private variable
-  ℓ ℓ′ : Level
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
 
 record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
   constructor _⟨⟩

lib/base/Haskell/Prelude.agda

@@ -6,7 +6,7 @@ open Haskell.Prim public using
   ( Type;
     Bool; True; False; Char; Integer;
     List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
+    UnsatisfiedConstraint; ⊥; iNumberNat; lengthNat;
     IsTrue; IsFalse; NonEmpty;
     All; allNil; allCons;
     Any; anyHere; anyThere;
@@ -43,6 +43,8 @@ open import Haskell.Prim.Traversable public
 open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
 open import Haskell.Prim.Word        public
 
+open import Haskell.Control.Exception
+
 -- Problematic features
 --  - [Partial]:  Could pass implicit/instance arguments to prove totality.
 --  - [Float]:    Or Float (Agda floats are Doubles)
@@ -127,6 +129,16 @@ lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
 lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 
+-------------------------------------------------
+-- Exception handling in the I/O monad
+
+IOError = IOException
+
+ioError : @0 {{MayThrow IOError}} → IOError → IO a
+ioError = throwIO
+
+postulate
+  userError : String → IOError
 
 -------------------------------------------------
 -- Unsafe functions

lib/base/Haskell/Prim.agda

@@ -23,7 +23,7 @@ open import Agda.Builtin.Strict     public
 open import Agda.Builtin.List       public
 
 variable
-  @0 ℓ : Level
+  @0 ℓ ℓ′ : Level
   a b c d e : Type
   f m s t : Type → Type
 
@@ -124,7 +124,7 @@ data IsFalse : Bool → Type where
 data NonEmpty {a : Type} : List a → Type where
   instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
 
-data TypeError (err : AgdaString) : Type where
+data UnsatisfiedConstraint (err : AgdaString) : Type where
 
 it : ∀ {@0 ℓ} {@0 a : Type ℓ} → ⦃ a ⦄ → a
 it ⦃ x ⦄ = x

lib/base/Haskell/Prim/Int.agda

@@ -103,7 +103,7 @@ showInt a = showInteger (intToInteger a)
 
 @0 IsNonNegativeInt : Int → Type
 IsNonNegativeInt a@(int64 _) =
-  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
+  if isNegativeInt a then UnsatisfiedConstraint (primStringAppend (primStringFromList (showInt a)) " is negative")
                      else ⊤
 
 intToNat : (a : Int) → @0 ⦃ IsNonNegativeInt a ⦄ → Nat

lib/base/Haskell/Prim/Integer.agda

@@ -103,4 +103,4 @@ isNegativeInteger (negsuc _) = True
 @0 IsNonNegativeInteger : Integer → Type
 IsNonNegativeInteger (pos _)      = ⊤
 IsNonNegativeInteger n@(negsuc _) =
-  TypeError (primStringAppend (primShowInteger n) (" is negative"))
+  UnsatisfiedConstraint (primStringAppend (primShowInteger n) (" is negative"))

lib/base/Haskell/System/Environment.agda

@@ -0,0 +1,18 @@
+
+open import Haskell.Prelude
+open import Haskell.Control.Exception
+
+module Haskell.System.Environment where
+
+postulate
+  getArgs : IO (List String)
+  getProgName : IO String
+  executablePath : Maybe (IO (Maybe FilePath))
+  getExecutablePath : IO FilePath
+  getEnv : @0 {{MayThrow IOException}} → String → IO String
+  lookupEnv : String → IO (Maybe String)
+  setEnv : @0 {{MayThrow IOException}} → String → String → IO ⊤
+  unsetEnv : @0 {{MayThrow IOException}} → String → IO ⊤
+  withArgs : List String → IO a → IO a
+  withProgName : String → IO a → IO a
+  getEnvironment : IO (List (String × String))

test/AllTests.agda

@@ -106,6 +106,7 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -209,4 +210,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate
 #-}

test/Assert.agda

@@ -4,7 +4,7 @@ open import Haskell.Control.Exception
 open import Haskell.Law.Ord
 open import Haskell.Extra.Dec
 
-subtractChecked : Nat → Nat → Nat
+subtractChecked : @0 {{MayThrow AssertionFailed}} → Nat → Nat → Nat
 subtractChecked x y = assert (IsFalse (x < y)) (x - y)
 
 {-# COMPILE AGDA2HS subtractChecked #-}

test/ParseOrValidate.agda

@@ -0,0 +1,57 @@
+{-# OPTIONS --erasure #-}
+
+open import Haskell.Prelude
+open import Haskell.Control.Exception
+open import Haskell.Control.Monad
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Erase
+open import Haskell.Extra.Refinement
+open import Haskell.System.Environment
+
+it : {{a}} → a
+it {{x}} = x
+
+{-# COMPILE AGDA2HS it inline #-}
+
+{-# TERMINATING #-}
+split : Char → String → List String
+split c s = case rest of λ where
+                []     → chunk ∷ []
+                (_ ∷ rest) → chunk ∷ split c rest
+  where
+    broken = break (_== c) s
+    chunk = fst broken
+    rest = snd broken
+
+{-# COMPILE AGDA2HS split #-}
+
+-- The below example is taken from the classic blog post by Alexis King
+-- "Parse, don't validate". Here I ignore her advice but instead implement
+-- a validation function that returns evidence of the property it checked.
+
+validateNonEmpty : @0 {{MayThrow IOException}} → (xs : List a) → IO (Erase (NonEmpty xs))
+validateNonEmpty [] = throwIO (userError "list cannot be empty")
+validateNonEmpty (x ∷ xs) = return it
+
+{-# COMPILE AGDA2HS validateNonEmpty #-}
+
+getConfigurationDirectories : @0 {{MayThrow IOException}} → IO (∃ (List FilePath) NonEmpty)
+getConfigurationDirectories = do
+  configDirsString <- getEnv "CONFIG_DIRS"
+  let configDirsList = split ',' configDirsString
+  validateNonEmpty configDirsList
+  pure (configDirsList ⟨⟩)
+
+{-# COMPILE AGDA2HS getConfigurationDirectories #-}
+
+-- TODO: implement this function?
+postulate
+  initializeCache : String → IO ⊤
+{-# COMPILE AGDA2HS initializeCache #-}
+
+main : @0 {{MayThrow IOException}} → IO ⊤
+main = do
+  configDirs ⟨ i ⟩ <- getConfigurationDirectories
+  initializeCache (head configDirs {{i}})
+
+{-# COMPILE AGDA2HS main #-}

test/RuntimeCast.agda

@@ -14,8 +14,8 @@ it : {{A}} → A
 it {{x}} = x
 
 data _~_ : (A : Set) (B : Set) → Set₁
-cast  : A ~ B → A → B
-cast' : A ~ B → B → A
+cast  : @0 {{MayThrow AssertionFailed}} → A ~ B → A → B
+cast' : @0 {{MayThrow AssertionFailed}} → A ~ B → B → A
 
 data _~_ where
   refl : A ~ A
@@ -78,7 +78,9 @@ module Sqrt where
 
   {-# COMPILE AGDA2HS eqr inline #-}
 
-  checkedSqrt : (x : Double) → ∃ Double (λ y → IsTrue (y >= 0) × IsTrue (abs (x - y * y) <= 0.01))
+  checkedSqrt : @0 {{MayThrow AssertionFailed}}
+              → (x : Double)
+              → ∃ Double (λ y → IsTrue (y >= 0) × IsTrue (abs (x - y * y) <= 0.01))
   checkedSqrt = cast eqr mySqrt
 
   {-# COMPILE AGDA2HS checkedSqrt #-}

test/golden/AllTests.hs

@@ -101,4 +101,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import ParseOrValidate