Tracked (and dispatchable) exception-handling with classy variants.

Oops.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

-- Classy exception-handling with variants. This module provides two functions,
-- 'throw' and 'catch', for working with variants as one may work with
-- exceptions both inside and outside of Haskell.
--
-- Examples are at the bottom, but I think the explanation is the interesting
-- part.

module Oops
  ( Variant
  , CouldBe (..)
  , Drop (..)
  ) where

import Data.Kind (Type)

-- 'Variant' is a generalised 'Either' type. Instead of being one type /or/
-- another, a 'Variant' could be anything within a list of types. We use 'Here'
-- and 'There' to act as a pointer to the appropriate type in the list. If you
-- match a @Here x :: Variant (t ': ts)@, the type of @x@ is @t@. If you match
-- a @There x :: Variant (t ': ts)@, the type of @x@ is further down the list.

-- The beauty of the 'throw' function is that you'll never have to write 'Here'
-- or 'There', of course - all this is an implementation detail :D

data Variant (xs :: [Type]) where
  Here :: x -> Variant (x ': xs)
  There :: Variant xs -> Variant (y ': xs)

-- I am /addicted/ to infix constraints (I like my predicates to read as
-- "naturally" as possible). This says that if a 'Variant' of types @xs@
-- contains an @x@ (i.e. that 'Variant' __could be__ holding an @x@), then we
-- can lift an @x@ into that variant (which we'll call 'throw'ing, for the sake
-- of the intuition).

class (xs :: [Type]) `CouldBe` (x :: Type) where
  throw :: x -> Variant xs

-- If the head of the types we're searching is the same as the type we want to
-- throw, then the job is straightforward!

instance (x ': xs) `CouldBe` x where
  throw = Here

-- If the head /doesn't/ match, we need to look further into the list. So, we
-- 'throw' for the tail list, and then stick a 'There' on the front to skip
-- over the type we're ignoring (@y@). This is @OVERLAPPABLE@ because anything
-- that matches the first instance would also match this one. However, we want
-- to express that the above instance should be given "priority" in these
-- cases.

instance {-# OVERLAPPABLE #-} xs `CouldBe` x
    => (y ': xs) `CouldBe` x where
  throw = There . throw

-- If we can 'throw' errors into our 'Variant', we should be able to 'catch'
-- them as well! This function takes a 'Variant' and removes a given type from
-- the list of possibilities. How does it do this? Well, if that type happens
-- to be the actual type of the value within the 'Variant', we get that value
-- back in a 'Left'. If not, we get the 'Variant' back in a 'Right', but
-- without that particular type in the list of possibilities. Given that
-- there's no way to build a @Variant '[]@, we can simply catch errors
-- one-by-one until we've covered everything.

class Drop x xs ys | x xs -> ys, x ys -> xs where
  catch :: Variant xs -> Either x (Variant ys)

-- First up, we need to supply an instance to 'catch' the first type in the
-- list. Two possibilities to handle here:
--
-- * The thing we have is a 'Here', and we've found the value. Cool, return the
--   value in a 'Left' and we're done!
-- 
-- * The thing we have is a 'There', and we /haven't/ found the value, which
--   means there must be a duplicate type in our list (or unification hasn't
--   worked in our favour). This might be irritating in other circumstances,
--   but it isn't necessarily a problem for us - we just keep recursing!

instance Drop x (x ': xs) xs where
  catch (Here  x ) = Left x
  catch (There xs) = Right xs

-- What if the head of the list /isn't/ the droid we're looking for? In this
-- case, we'll need another @OVERLAPPABLE@ constraint to recurse down the tail.
-- However, we hit another problem (try changing the pragma!)
--
-- (If you want to follow along, check out
-- https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-class-extensions.html#instance-overlap
-- for the instance resolution rules).
--
-- Let's say we need to solve a constraint like @Drop String (String ': e) e@.
-- The head definitely matches the above instance, and this one is
-- @OVERLAPPABLE@, so job done, right? ... Not quite.
--
-- Firstly, GHC finds all the instances that would work here. In this case, it
-- finds two. It can't eliminate either one because neither are substitutions
-- of the other. In other words, the first instance doesn't require the second
-- list to be non-empty (unlike @z ': ys@ here), and the second instance
-- doesn't require the head type to match. Thus, GHC continues to believe that
-- both are good candidates.
--
-- Because both /could/ still match our constraint, but neither can be
-- eliminated, GHC gives up and bails out. However, rule three on the instance
-- resolution step list says:
--
-- > "If exactly one non-incoherent candidate remains, select it. If all
--   remaining candidates are incoherent, select an arbitrary one."
--
-- If we only have one incoherent instance, this choice is never arbitrary! All
-- it means is that, regardless of the fact that one isn't more "specific" than
-- the other, it will always be ignored if the other instance is applicable.
--
-- Because of this, our second instance is /only/ used when the head doesn't
-- match, and the first head is /only/ used when it does. GHC is happy, we're
-- happy, and we've only written the scary word once!

instance {-# INCOHERENT #-} (y ~ z, Drop x xs ys)
    => Drop x (y ': xs) (z ': ys) where
  catch (There xs) = fmap There (catch xs)

---


-- Here's a nice little demo of the code in action: we can list the things that
-- @e@ /could be/ in constraints, and we never have to be explicit about our
-- concrete set of possibilities until we get into actual top-level business
-- logic. No upcasting, no unification errors, etc!

f :: (e `CouldBe` String, e `CouldBe` Bool) => Variant e
f = throw True

-- The /much more exciting/ part of this demo is here. Notice that one of our
-- constraints has disappeared, and we haven't added a @Drop@ constraint. GHC
-- is clever enough to partially-specialise @e@ here to @(String ': etc)@,
-- which is enough to know which @Drop@ instance to choose (thanks to some
-- @INCOHERENT@ magic!) and can hence discharge the constraints before knowing
-- anything more about @e@! It's a magical beast.

g :: e `CouldBe` Bool => Either String (Variant e)
g = catch @String f