Optional function arguments in Idris

Optional.idr

interface Optional a t where
    optional : t -> Maybe a

Optional a (Maybe a) where
    optional x = x

Optional a a where
    optional x = Just x

Optional a () where
    optional _ = Nothing

Optional a (Either e a) where
    optional (Right x) = Just x
    optional _ = Nothing


f : Optional Integer t => t -> String
f x =
    case the (Maybe Integer) (optional x) of
        Just x => "number " ++ show x
        Nothing => "nothing"


examples : List String
examples =
    [ f 5
    , f (Just 3)
    , f Nothing
    , f ()
    , f (Left "lofasz")
    , f (the (Either () Integer) (Right 4))
    ]


default : Optional a t => a -> t -> a
default {a} def x =
    case (the (Maybe a) (optional x)) of
        Just x => x
        Nothing => def


g : Optional Integer t => t -> String
g x =
    "number " ++ show (default 0 x)


examples' : List String
examples' =
    [ g 4
    , g Nothing
    ]