diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,13 +1,19 @@
-# 0.3.0
-
-- Simplify API
-- Support -vv -vvv verbosity
-- Improve help message
-
-# 0.2.0
-
-- Verbosity support
-
-# 0.1.0
-
-- First release
+# 0.3.1
+
+- Allow False as a default value for Bool arguments [#2](https://github.com/tanakh/optparse-declarative/pull/2)
+- Make `[]` a `IsCmd` instance [#6](https://github.com/tanakh/optparse-declarative/pull/6)
+- Fix typo in README [#1](https://github.com/tanakh/optparse-declarative/pull/1)
+
+# 0.3.0
+
+- Simplify API
+- Support -vv -vvv verbosity
+- Improve help message
+
+# 0.2.0
+
+- Verbosity support
+
+# 0.1.0
+
+- First release
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,20 +1,20 @@
-Copyright (c) 2015 Hideyuki Tanaka
-
-Permission is hereby granted, free of charge, to any person obtaining
-a copy of this software and associated documentation files (the
-"Software"), to deal in the Software without restriction, including
-without limitation the rights to use, copy, modify, merge, publish,
-distribute, sublicense, and/or sell copies of the Software, and to
-permit persons to whom the Software is furnished to do so, subject to
-the following conditions:
-
-The above copyright notice and this permission notice shall be included
-in all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
-CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
-TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
-SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+Copyright (c) 2020 Kazuki Okamoto, 2015 Hideyuki Tanaka
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,7 @@
 # optparse-declarative
 
+[![Hackage](https://matrix.hackage.haskell.org/api/v2/packages/optparse-declarative/badge)](http://hackage.haskell.org/package/optparse-declarative) [![GitHub Actions: test](https://github.com/tanakh/optparse-declarative/workflows/test/badge.svg)](https://github.com/tanakh/optparse-declarative/actions?query=workflow%3Atest) [![Join the chat at https://gitter.im/optparse-declarative/community](https://badges.gitter.im/optparse-declarative/community.svg)](https://gitter.im/optparse-declarative/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
+
 `optparse-declarative` is a declarative and easy to use command-line option parser.
 
 # Install
@@ -71,7 +73,7 @@
 Goodbye, World!
 ```
 
-## Writing multiple sum-commands
+## Writing multiple sub-commands
 
 You can write (nested) sub-commands.
 
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,2 @@
-import Distribution.Simple
-main = defaultMain
+import Distribution.Simple
+main = defaultMain
diff --git a/example/nonstrargs.hs b/example/nonstrargs.hs
new file mode 100644
--- /dev/null
+++ b/example/nonstrargs.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds #-}
+
+import           Control.Monad.Trans
+import           Options.Declarative
+
+sum' :: Arg "N" Int
+     -> Arg "NS" [Int]
+     -> Cmd "Simple greeting example" ()
+sum' n ns =
+    liftIO $ putStrLn $ show (get n) ++ ", " ++ show (sum $ get ns)
+
+main :: IO ()
+main = run_ sum'
diff --git a/example/simple.hs b/example/simple.hs
--- a/example/simple.hs
+++ b/example/simple.hs
@@ -1,13 +1,13 @@
-{-# LANGUAGE DataKinds #-}
-
-import           Control.Monad.Trans
-import           Options.Declarative
-
-greet :: Flag "g" '["greet"] "STRING" "greeting message" (Def "Hello" String)
-      -> Arg "NAME" String
-      -> Cmd "Simple greeting example" ()
-greet msg name =
-    liftIO $ putStrLn $ get msg ++ ", " ++ get name ++ "!"
-
-main :: IO ()
-main = run_ greet
+{-# LANGUAGE DataKinds #-}
+
+import           Control.Monad.Trans
+import           Options.Declarative
+
+greet :: Flag "g" '["greet"] "STRING" "greeting message" (Def "Hello" String)
+      -> Arg "NAME" String
+      -> Cmd "Simple greeting example" ()
+greet msg name =
+    liftIO $ putStrLn $ get msg ++ ", " ++ get name ++ "!"
+
+main :: IO ()
+main = run_ greet
diff --git a/example/subcmd.hs b/example/subcmd.hs
--- a/example/subcmd.hs
+++ b/example/subcmd.hs
@@ -1,36 +1,36 @@
-{-# LANGUAGE DataKinds #-}
-
-import           Control.Monad.Trans
-import           Options.Declarative
-
-greet :: Flag "g" '["greet"] "STRING" "greeting message" (Def "Hello" String)
-      -> Flag "" '["decolate"] "" "decolate message" Bool
-      -> Arg "NAME" String
-      -> Cmd "Greeting command" ()
-greet msg deco name = do
-    let f x | get deco = "*** " ++ x ++ " ***"
-            | otherwise = x
-    liftIO $ putStrLn $ f $ get msg ++ ", " ++ get name ++ "!"
-
-connect :: Flag "h" '["host"] "HOST" "host name"   (Def "localhost" String)
-        -> Flag "p" '["port"] "PORT" "port number" (Def "8080"      Int   )
-        -> Cmd "Connect command" ()
-connect host port = do
-    let addr = get host ++ ":" ++ show (get port)
-    liftIO $ putStrLn $ "connect to " ++ addr
-
-getOptExample
-    :: Flag "o" '["output"] "FILE" "output FILE" (Def "stdout" String)
-    -> Flag "c" '[] "FILE" "input FILE" (Def "stdin" String)
-    -> Flag "L" '["libdir"] "DIR" "library directory" String
-    -> Cmd "GetOpt example" ()
-getOptExample output input libdir =
-    liftIO $ print (get output, get input, get libdir)
-
-main :: IO ()
-main = run_ $
-    Group "Test program for sub commands"
-    [ subCmd "greet"   greet
-    , subCmd "connect" connect
-    , subCmd "getopt"  getOptExample
-    ]
+{-# LANGUAGE DataKinds #-}
+
+import           Control.Monad.Trans
+import           Options.Declarative
+
+greet :: Flag "g" '["greet"] "STRING" "greeting message" (Def "Hello" String)
+      -> Flag "" '["decolate"] "" "decolate message" Bool
+      -> Arg "NAME" String
+      -> Cmd "Greeting command" ()
+greet msg deco name = do
+    let f x | get deco = "*** " ++ x ++ " ***"
+            | otherwise = x
+    liftIO $ putStrLn $ f $ get msg ++ ", " ++ get name ++ "!"
+
+connect :: Flag "h" '["host"] "HOST" "host name"   (Def "localhost" String)
+        -> Flag "p" '["port"] "PORT" "port number" (Def "8080"      Int   )
+        -> Cmd "Connect command" ()
+connect host port = do
+    let addr = get host ++ ":" ++ show (get port)
+    liftIO $ putStrLn $ "connect to " ++ addr
+
+getOptExample
+    :: Flag "o" '["output"] "FILE" "output FILE" (Def "stdout" String)
+    -> Flag "c" '[] "FILE" "input FILE" (Def "stdin" String)
+    -> Flag "L" '["libdir"] "DIR" "library directory" String
+    -> Cmd "GetOpt example" ()
+getOptExample output input libdir =
+    liftIO $ print (get output, get input, get libdir)
+
+main :: IO ()
+main = run_ $
+    Group "Test program for sub commands"
+    [ subCmd "greet"   greet
+    , subCmd "connect" connect
+    , subCmd "getopt"  getOptExample
+    ]
diff --git a/example/verbose.hs b/example/verbose.hs
--- a/example/verbose.hs
+++ b/example/verbose.hs
@@ -1,13 +1,13 @@
-{-# LANGUAGE DataKinds #-}
-
-import           Options.Declarative
-
-test :: Cmd "verbosity test" ()
-test = do
-    logStr 0 "verbosity level 0"
-    logStr 1 "verbosity level 1"
-    logStr 2 "verbosity level 2"
-    logStr 3 "verbosity level 3"
-
-main :: IO ()
-main = run_ test
+{-# LANGUAGE DataKinds #-}
+
+import           Options.Declarative
+
+test :: Cmd "verbosity test" ()
+test = do
+    logStr 0 "verbosity level 0"
+    logStr 1 "verbosity level 1"
+    logStr 2 "verbosity level 2"
+    logStr 3 "verbosity level 3"
+
+main :: IO ()
+main = run_ test
diff --git a/optparse-declarative.cabal b/optparse-declarative.cabal
--- a/optparse-declarative.cabal
+++ b/optparse-declarative.cabal
@@ -1,28 +1,28 @@
-name:                optparse-declarative
-version:             0.3.0
-synopsis:            Declarative command line option parser
-description:         Declarative and easy to use command line option parser
-homepage:            https://github.com/tanakh/optparse-declarative
-license:             MIT
-license-file:        LICENSE
-author:              Hideyuki Tanaka
-maintainer:          tanaka.hideyuki@gmail.com
-copyright:           (c) Hideyuki Tanaka 2015
-category:            System
-build-type:          Simple
-cabal-version:       >=1.10
-
-extra-source-files:  README.md
-                     ChangeLog.md
-                     example/*.hs
-
-source-repository head
-  type:     git
-  location: https://github.com/tanakh/optparse-declarative.git
-
-library
-  hs-source-dirs:      src
-  exposed-modules:     Options.Declarative
-  default-language:    Haskell2010
-  build-depends:       base >=4.7 && <5
-                     , mtl
+cabal-version:       2.2
+name:                optparse-declarative
+version:             0.3.1
+synopsis:            Declarative command line option parser
+description:         Declarative and easy to use command line option parser
+homepage:            https://github.com/tanakh/optparse-declarative
+license:             MIT
+license-file:        LICENSE
+author:              Hideyuki Tanaka
+maintainer:          tanaka.hideyuki@gmail.com, kazuki.okamoto@kakkun61.com
+copyright:           2020 Kazuki Okamoto (岡本和樹), (c) Hideyuki Tanaka 2015
+category:            System
+build-type:          Simple
+
+extra-source-files:  README.md
+                     ChangeLog.md
+                     example/*.hs
+
+source-repository head
+  type:     git
+  location: https://github.com/tanakh/optparse-declarative.git
+
+library
+  hs-source-dirs:   src
+  exposed-modules:  Options.Declarative
+  build-depends:    base >=4.7 && <5
+                  , mtl
+  default-language: Haskell2010
diff --git a/src/Options/Declarative.hs b/src/Options/Declarative.hs
--- a/src/Options/Declarative.hs
+++ b/src/Options/Declarative.hs
@@ -1,363 +1,383 @@
-{-# LANGUAGE DataKinds                  #-}
-{-# LANGUAGE DefaultSignatures          #-}
-{-# LANGUAGE ExistentialQuantification  #-}
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE FlexibleInstances          #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE KindSignatures             #-}
-{-# LANGUAGE MultiWayIf                 #-}
-{-# LANGUAGE PolyKinds                  #-}
-{-# LANGUAGE RankNTypes                 #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE TypeFamilies               #-}
-{-# LANGUAGE TypeOperators              #-}
-
--- | Declarative options parser
-
-module Options.Declarative (
-    -- * Command type
-    IsCmd,
-    Cmd,
-    logStr,
-    getVerbosity,
-    getLogger,
-
-    -- * Argument definition tools
-    Option(..),
-    Flag,
-    Arg,
-
-    -- * Defining argment types
-    ArgRead(..),
-    Def,
-
-    -- * Subcommands support
-    Group(..),
-    SubCmd, subCmd,
-
-    -- * Run a command
-    run, run_,
-    ) where
-
-import           Control.Applicative
-import           Control.Monad
-import           Control.Monad.Reader
-import           Control.Monad.Trans
-import           Data.List
-import           Data.Maybe
-import           Data.Proxy
-import           GHC.TypeLits
-import           System.Console.GetOpt
-import           System.Environment
-import           System.Exit
-import           System.IO
-import           Text.Read
-
--- | Command line option
-class Option a where
-    -- | Type of the argument' value
-    type Value a :: *
-    -- | Get the argument' value
-    get :: a -> Value a
-
--- | Named argument
-newtype Flag (shortNames  :: Symbol  )
-             (longNames   :: [Symbol])
-             (placeholder :: Symbol  )
-             (help        :: Symbol  )
-             a
-    = Flag { getFlag :: a }
-
--- | Unnamed argument
-newtype Arg (placeholder :: Symbol) a = Arg { getArg :: a }
-
-instance ArgRead a => Option (Flag _a _b _c _d a) where
-    type Value (Flag _a _b _c _d a) = Unwrap a
-    get = unwrap . getFlag
-
-instance Option (Arg _a a) where
-    type Value (Arg _a a) = a
-    get = getArg
-
--- | Command line option's annotated types
-class ArgRead a where
-    -- | Type of the argument
-    type Unwrap a :: *
-    type Unwrap a = a
-
-    -- | Get the argument's value
-    unwrap :: a -> Unwrap a
-    default unwrap :: a ~ Unwrap a => a -> Unwrap a
-    unwrap = id
-
-    -- | Argument parser
-    argRead :: Maybe String -> Maybe a
-    default argRead :: Read a => Maybe String -> Maybe a
-    argRead s = readMaybe =<< s
-
-    -- | Indicate this argument is mandatory
-    needArg :: Proxy a -> Bool
-    needArg _ = True
-
-instance ArgRead Int
-
-instance ArgRead Integer
-
-instance ArgRead Double
-
-instance ArgRead String where
-    argRead = id
-
-instance ArgRead Bool where
-    argRead Nothing = Just False
-    argRead (Just "t") = Just True
-    argRead _ = Nothing
-
-    needArg _ = False
-
-instance ArgRead a => ArgRead (Maybe a) where
-    argRead Nothing = Just Nothing
-    argRead (Just a) = Just <$> argRead (Just a)
-
--- | The argument which has defalut value
-newtype Def (defaultValue :: Symbol) a =
-    Def { getDef :: a }
-
-instance (KnownSymbol defaultValue, ArgRead a) => ArgRead (Def defaultValue a) where
-    type Unwrap (Def defaultValue a) = Unwrap a
-    unwrap = unwrap . getDef
-
-    argRead s =
-        let s' = fromMaybe (symbolVal (Proxy :: Proxy defaultValue)) s
-        in Def <$> argRead (Just s')
-
--- | Command
-newtype Cmd (help :: Symbol) a =
-    Cmd { unCmd :: ReaderT Int IO a }
-    deriving (Functor, Applicative, Monad, MonadIO)
-
--- | Output string when the verbosity level is greater than or equal to `logLevel`
-logStr :: Int         -- ^ Verbosity Level
-       -> String      -- ^ Message
-       -> Cmd help ()
-logStr logLevel msg = do
-    l <- getLogger
-    l logLevel msg
-
--- | Return the verbosity level ('--verbosity=n')
-getVerbosity :: Cmd help Int
-getVerbosity = Cmd ask
-
--- | Retrieve the logger function
-getLogger :: MonadIO m => Cmd a (Int -> String -> m ())
-getLogger = do
-    verbosity <- getVerbosity
-    return $ \logLevel msg -> when (verbosity >= logLevel) $ liftIO $ putStrLn msg
-
--- | Command group
-data Group =
-    Group
-    { groupHelp :: String
-    , groupCmds :: [SubCmd]
-    }
-
--- | Sub command
-data SubCmd = forall c. IsCmd c => SubCmd String c
-
--- | Command class
-class IsCmd c where
-    getCmdHelp  :: c -> String
-    default getCmdHelp :: (c ~ (a -> b), IsCmd b) => c -> String
-    getCmdHelp f = getCmdHelp $ f undefined
-
-    getOptDescr :: c -> [OptDescr (String, String)]
-    default getOptDescr :: (c ~ (a -> b), IsCmd b) => c -> [OptDescr (String, String)]
-    getOptDescr f = getOptDescr $ f undefined
-
-    getUsageHeader :: c -> String -> String
-    default getUsageHeader :: (c ~ (a -> b), IsCmd b) => c -> String -> String
-    getUsageHeader f = getUsageHeader $ f undefined
-
-    getUsageFooter :: c -> String -> String
-    default getUsageFooter :: (c ~ (a -> b), IsCmd b) => c -> String -> String
-    getUsageFooter f = getUsageFooter $ f undefined
-
-    runCmd :: c
-           -> [String]            -- ^ Command name
-           -> Maybe String        -- ^ Version
-           -> [(String, String)]  -- ^ Options
-           -> [String]            -- ^ Non options
-           -> [String]            -- ^ Unrecognized options
-           -> IO ()
-
-class KnownSymbols (s :: [Symbol]) where
-    symbolVals :: Proxy s -> [String]
-
-instance KnownSymbols '[] where
-    symbolVals _ = []
-
-instance (KnownSymbol s, KnownSymbols ss) => KnownSymbols (s ': ss) where
-    symbolVals _ = symbolVal (Proxy :: Proxy s) : symbolVals (Proxy :: Proxy ss)
-
-instance ( KnownSymbol shortNames
-         , KnownSymbols longNames
-         , KnownSymbol placeholder
-         , KnownSymbol help
-         , ArgRead a
-         , IsCmd c )
-         => IsCmd (Flag shortNames longNames placeholder help a -> c) where
-    getOptDescr f =
-        let flagname = head $
-                       symbolVals (Proxy :: Proxy longNames) ++
-                       [ [c] | c <- symbolVal (Proxy :: Proxy shortNames) ]
-        in Option
-            (symbolVal (Proxy :: Proxy shortNames))
-            (symbolVals (Proxy :: Proxy longNames))
-            (if needArg (Proxy :: Proxy a)
-             then ReqArg
-                  (flagname, )
-                  (symbolVal (Proxy :: Proxy placeholder))
-             else NoArg
-                  (flagname, "t"))
-            (symbolVal (Proxy :: Proxy help))
-        : getOptDescr (f undefined)
-
-    runCmd f name mbver options nonOptions unrecognized =
-        let flagname = head $
-                       symbolVals (Proxy :: Proxy longNames) ++
-                       [ [c] | c <- symbolVal (Proxy :: Proxy shortNames) ]
-            mbs = lookup flagname options
-        in case (argRead mbs, mbs) of
-            (Nothing, Nothing) ->
-                errorExit name $ "flag must be specified: --" ++ flagname
-            (Nothing, Just s) ->
-                errorExit name $ "bad argument: --" ++ flagname ++ "=" ++ s
-            (Just arg, _) ->
-                runCmd (f $ Flag arg) name mbver options nonOptions unrecognized
-
-instance ( KnownSymbol placeholder, IsCmd c )
-         => IsCmd (Arg placeholder String -> c) where
-    getUsageHeader f prog =
-        " " ++ symbolVal (Proxy :: Proxy placeholder) ++ getUsageHeader (f undefined) prog
-
-    runCmd f name mbver options nonOptions unrecognized =
-        case nonOptions of
-            [] -> errorExit name "not enough arguments"
-            (opt: rest) ->
-                case argRead (Just opt) of
-                    Nothing ->
-                        errorExit name $ "bad argument: " ++ opt
-                    Just arg ->
-                        runCmd (f $ Arg arg) name mbver options rest unrecognized
-
-instance ( KnownSymbol placeholder, IsCmd c )
-         => IsCmd (Arg placeholder [String] -> c) where
-    getUsageHeader f prog =
-        " " ++ symbolVal (Proxy :: Proxy placeholder) ++ getUsageHeader (f undefined) prog
-
-    runCmd f name mbver options nonOptions unrecognized =
-        runCmd (f $ Arg nonOptions) name mbver options [] unrecognized
-
-instance KnownSymbol help => IsCmd (Cmd help ()) where
-    getCmdHelp  _ = symbolVal (Proxy :: Proxy help)
-    getOptDescr _ = []
-
-    getUsageHeader _ _ = ""
-    getUsageFooter _ _ = ""
-
-    runCmd (Cmd m) name _ options nonOptions unrecognized =
-        case (options, nonOptions, unrecognized) of
-            (_, [], []) -> do
-                let verbosityLevel = fromMaybe 0 $ do
-                        s <- lookup "verbose" options
-                        if | null s -> return 1
-                           | all (== 'v') s -> return $ length s + 1
-                           | otherwise -> readMaybe s
-                runReaderT m verbosityLevel
-
-            _ -> do
-                forM_ nonOptions $ \o ->
-                    errorExit name $ "unrecognized argument '" ++ o ++ "'"
-                forM_ unrecognized $ \o ->
-                    errorExit name $ "unrecognized option '" ++ o ++ "'"
-                exitFailure
-
-instance IsCmd Group where
-    getCmdHelp = groupHelp
-    getOptDescr _ = []
-
-    getUsageHeader _ _ = " <COMMAND> [ARGS...]"
-    getUsageFooter g _ = unlines $
-        [ ""
-        , "Commands: "
-        ] ++
-        [ "  " ++ name ++ replicate (12 - length name) ' ' ++ getCmdHelp c
-        | SubCmd name c <- groupCmds g
-        ]
-
-    runCmd g name mbver _options (cmd: nonOptions) unrecognized =
-        case [ SubCmd subname c | SubCmd subname c <- groupCmds g, subname == cmd ] of
-           [SubCmd subname c] ->
-               run' c (name ++ [subname]) mbver (nonOptions ++ unrecognized)
-           _ ->
-               errorExit name $ "unrecognized command: " ++ cmd
-    runCmd _ name _ _ _ _ =
-        errorExit name "no command given"
-
--- | Make a sub command
-subCmd :: IsCmd c => String -> c -> SubCmd
-subCmd = SubCmd
-
--- runner
-
-run' :: IsCmd c => c -> [String] -> Maybe String -> [String] -> IO ()
-run' cmd name mbver args = do
-    let optDescr =
-            getOptDescr cmd
-            ++ [ Option "?" ["help"]    (NoArg ("help",    "t")) "display this help and exit" ]
-            ++ [ Option "V" ["version"] (NoArg ("version", "t")) "output version information and exit"
-               | isJust mbver ]
-            ++ [ Option "v" ["verbose"] (OptArg (\arg -> ("verbose", fromMaybe "" arg)) "n") "set verbosity level" ]
-
-        prog     = unwords name
-        vermsg   = prog ++ maybe "" (" version " ++) mbver
-        header = "Usage: " ++ prog ++ " [OPTION...]" ++ getUsageHeader cmd prog ++ "\n" ++
-                 "  " ++ getCmdHelp cmd ++ "\n\n" ++
-                 "Options:"
-
-        usage    =
-            usageInfo header optDescr ++
-            getUsageFooter cmd prog
-
-    case getOpt' RequireOrder optDescr args of
-        (options, nonOptions, unrecognized, errors)
-            | not $ null errors ->
-                  errorExit name $ intercalate ", " errors
-            | isJust (lookup "help" options) -> do
-                  putStr usage
-                  exitSuccess
-            | isJust (lookup "version" options) -> do
-                  putStrLn vermsg
-                  exitSuccess
-            | otherwise ->
-                  runCmd cmd name mbver options nonOptions unrecognized
-
--- | Run a command with specifying program name and version
-run :: IsCmd c => String -> Maybe String -> c -> IO ()
-run progName progVer cmd =
-    run' cmd [progName] progVer =<< getArgs
-
--- | Run a command
-run_ :: IsCmd c => c -> IO ()
-run_ cmd = do
-    progName <- getProgName
-    run progName Nothing cmd
-
-errorExit :: [String] -> String -> IO ()
-errorExit name msg = do
-    let prog = unwords name
-    hPutStrLn stderr $ prog ++ ": " ++ msg
-    hPutStrLn stderr $ "Try '" ++ prog ++ " --help' for more information."
-    exitFailure
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE ExistentialQuantification  #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE MultiWayIf                 #-}
+{-# LANGUAGE PolyKinds                  #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+
+-- | Declarative options parser
+
+module Options.Declarative (
+    -- * Command type
+    IsCmd,
+    Cmd,
+    logStr,
+    getVerbosity,
+    getLogger,
+
+    -- * Argument definition tools
+    Option(..),
+    Flag,
+    Arg,
+
+    -- * Defining argment types
+    ArgRead(..),
+    Def,
+
+    -- * Subcommands support
+    Group(..),
+    SubCmd, subCmd,
+
+    -- * Run a command
+    run, run_,
+    ) where
+
+import           Control.Applicative
+import           Control.Monad
+import           Control.Monad.Reader
+import           Control.Monad.Trans
+import           Data.List
+import           Data.Maybe
+import           Data.Proxy
+import           GHC.TypeLits
+import           System.Console.GetOpt
+import           System.Environment
+import           System.Exit
+import           System.IO
+import           Text.Read
+
+-- | Command line option
+class Option a where
+    -- | Type of the argument' value
+    type Value a :: *
+    -- | Get the argument' value
+    get :: a -> Value a
+
+-- | Named argument
+newtype Flag (shortNames  :: Symbol  )
+             (longNames   :: [Symbol])
+             (placeholder :: Symbol  )
+             (help        :: Symbol  )
+             a
+    = Flag { getFlag :: a }
+
+-- | Unnamed argument
+newtype Arg (placeholder :: Symbol) a = Arg { getArg :: a }
+
+instance ArgRead a => Option (Flag _a _b _c _d a) where
+    type Value (Flag _a _b _c _d a) = Unwrap a
+    get = unwrap . getFlag
+
+instance Option (Arg _a a) where
+    type Value (Arg _a a) = a
+    get = getArg
+
+-- | Command line option's annotated types
+class ArgRead a where
+    -- | Type of the argument
+    type Unwrap a :: *
+    type Unwrap a = a
+
+    -- | Get the argument's value
+    unwrap :: a -> Unwrap a
+    default unwrap :: a ~ Unwrap a => a -> Unwrap a
+    unwrap = id
+
+    -- | Argument parser
+    argRead :: Maybe String -> Maybe a
+    default argRead :: Read a => Maybe String -> Maybe a
+    argRead s = readMaybe =<< s
+
+    -- | Indicate this argument is mandatory
+    needArg :: Proxy a -> Bool
+    needArg _ = True
+
+instance ArgRead Int
+
+instance ArgRead Integer
+
+instance ArgRead Double
+
+instance ArgRead String where
+    argRead = id
+
+instance ArgRead Bool where
+    argRead Nothing = Just False
+    argRead (Just "f") = Just False
+    argRead (Just "t") = Just True
+    argRead _ = Nothing
+
+    needArg _ = False
+
+instance ArgRead a => ArgRead (Maybe a) where
+    argRead Nothing = Just Nothing
+    argRead (Just a) = Just <$> argRead (Just a)
+
+-- | The argument which has defalut value
+newtype Def (defaultValue :: Symbol) a =
+    Def { getDef :: a }
+
+instance (KnownSymbol defaultValue, ArgRead a) => ArgRead (Def defaultValue a) where
+    type Unwrap (Def defaultValue a) = Unwrap a
+    unwrap = unwrap . getDef
+
+    argRead s =
+        let s' = fromMaybe (symbolVal (Proxy :: Proxy defaultValue)) s
+        in Def <$> argRead (Just s')
+
+-- | Command
+newtype Cmd (help :: Symbol) a =
+    Cmd { unCmd :: ReaderT Int IO a }
+    deriving (Functor, Applicative, Monad, MonadIO)
+
+-- | Output string when the verbosity level is greater than or equal to `logLevel`
+logStr :: Int         -- ^ Verbosity Level
+       -> String      -- ^ Message
+       -> Cmd help ()
+logStr logLevel msg = do
+    l <- getLogger
+    l logLevel msg
+
+-- | Return the verbosity level ('--verbosity=n')
+getVerbosity :: Cmd help Int
+getVerbosity = Cmd ask
+
+-- | Retrieve the logger function
+getLogger :: MonadIO m => Cmd a (Int -> String -> m ())
+getLogger = do
+    verbosity <- getVerbosity
+    return $ \logLevel msg -> when (verbosity >= logLevel) $ liftIO $ putStrLn msg
+
+-- | Command group
+data Group =
+    Group
+    { groupHelp :: String
+    , groupCmds :: [SubCmd]
+    }
+
+-- | Sub command
+data SubCmd = forall c. IsCmd c => SubCmd String c
+
+-- | Command class
+class IsCmd c where
+    getCmdHelp  :: c -> String
+    default getCmdHelp :: (c ~ (a -> b), IsCmd b) => c -> String
+    getCmdHelp f = getCmdHelp $ f undefined
+
+    getOptDescr :: c -> [OptDescr (String, String)]
+    default getOptDescr :: (c ~ (a -> b), IsCmd b) => c -> [OptDescr (String, String)]
+    getOptDescr f = getOptDescr $ f undefined
+
+    getUsageHeader :: c -> String -> String
+    default getUsageHeader :: (c ~ (a -> b), IsCmd b) => c -> String -> String
+    getUsageHeader f = getUsageHeader $ f undefined
+
+    getUsageFooter :: c -> String -> String
+    default getUsageFooter :: (c ~ (a -> b), IsCmd b) => c -> String -> String
+    getUsageFooter f = getUsageFooter $ f undefined
+
+    runCmd :: c
+           -> [String]            -- ^ Command name
+           -> Maybe String        -- ^ Version
+           -> [(String, String)]  -- ^ Options
+           -> [String]            -- ^ Non options
+           -> [String]            -- ^ Unrecognized options
+           -> IO ()
+
+class KnownSymbols (s :: [Symbol]) where
+    symbolVals :: Proxy s -> [String]
+
+instance KnownSymbols '[] where
+    symbolVals _ = []
+
+instance (KnownSymbol s, KnownSymbols ss) => KnownSymbols (s ': ss) where
+    symbolVals _ = symbolVal (Proxy :: Proxy s) : symbolVals (Proxy :: Proxy ss)
+
+instance ( KnownSymbol shortNames
+         , KnownSymbols longNames
+         , KnownSymbol placeholder
+         , KnownSymbol help
+         , ArgRead a
+         , IsCmd c )
+         => IsCmd (Flag shortNames longNames placeholder help a -> c) where
+    getOptDescr f =
+        let flagname = head $
+                       symbolVals (Proxy :: Proxy longNames) ++
+                       [ [c] | c <- symbolVal (Proxy :: Proxy shortNames) ]
+        in Option
+            (symbolVal (Proxy :: Proxy shortNames))
+            (symbolVals (Proxy :: Proxy longNames))
+            (if needArg (Proxy :: Proxy a)
+             then ReqArg
+                  (flagname, )
+                  (symbolVal (Proxy :: Proxy placeholder))
+             else NoArg
+                  (flagname, "t"))
+            (symbolVal (Proxy :: Proxy help))
+        : getOptDescr (f undefined)
+
+    runCmd f name mbver options nonOptions unrecognized =
+        let flagname = head $
+                       symbolVals (Proxy :: Proxy longNames) ++
+                       [ [c] | c <- symbolVal (Proxy :: Proxy shortNames) ]
+            mbs = lookup flagname options
+        in case (argRead mbs, mbs) of
+            (Nothing, Nothing) ->
+                errorExit name $ "flag must be specified: --" ++ flagname
+            (Nothing, Just s) ->
+                errorExit name $ "bad argument: --" ++ flagname ++ "=" ++ s
+            (Just arg, _) ->
+                runCmd (f $ Flag arg) name mbver options nonOptions unrecognized
+
+instance {-# OVERLAPPABLE #-}
+         ( KnownSymbol placeholder, ArgRead a, IsCmd c )
+         => IsCmd (Arg placeholder a -> c) where
+    getUsageHeader = getUsageHeaderOne (Proxy :: Proxy placeholder)
+
+    runCmd = runCmdOne
+
+instance {-# OVERLAPPING #-}
+         ( KnownSymbol placeholder, IsCmd c )
+         => IsCmd (Arg placeholder String -> c) where
+    getUsageHeader = getUsageHeaderOne (Proxy :: Proxy placeholder)
+
+    runCmd = runCmdOne
+
+getUsageHeaderOne :: ( KnownSymbol placeholder, ArgRead a, IsCmd c )
+                  => Proxy placeholder -> (Arg placeholder a -> c) -> String -> String
+getUsageHeaderOne proxy f prog =
+    " " ++ symbolVal proxy ++ getUsageHeader (f undefined) prog
+
+runCmdOne f name mbver options nonOptions unrecognized =
+    case nonOptions of
+        [] -> errorExit name "not enough arguments"
+        (opt: rest) ->
+            case argRead (Just opt) of
+                Nothing ->
+                    errorExit name $ "bad argument: " ++ opt
+                Just arg ->
+                    runCmd (f $ Arg arg) name mbver options rest unrecognized
+
+instance {-# OVERLAPPING #-}
+         ( KnownSymbol placeholder, ArgRead a, IsCmd c )
+         => IsCmd (Arg placeholder [a] -> c) where
+    getUsageHeader f prog =
+        " " ++ symbolVal (Proxy :: Proxy placeholder) ++ getUsageHeader (f undefined) prog
+
+    runCmd f name mbver options nonOptions unrecognized =
+        case traverse argRead $ Just <$> nonOptions of
+            Nothing ->
+                errorExit name $ "bad arguments: " ++ unwords nonOptions
+            Just opts ->
+                runCmd (f $ Arg opts) name mbver options [] unrecognized
+
+instance KnownSymbol help => IsCmd (Cmd help ()) where
+    getCmdHelp  _ = symbolVal (Proxy :: Proxy help)
+    getOptDescr _ = []
+
+    getUsageHeader _ _ = ""
+    getUsageFooter _ _ = ""
+
+    runCmd (Cmd m) name _ options nonOptions unrecognized =
+        case (options, nonOptions, unrecognized) of
+            (_, [], []) -> do
+                let verbosityLevel = fromMaybe 0 $ do
+                        s <- lookup "verbose" options
+                        if | null s -> return 1
+                           | all (== 'v') s -> return $ length s + 1
+                           | otherwise -> readMaybe s
+                runReaderT m verbosityLevel
+
+            _ -> do
+                forM_ nonOptions $ \o ->
+                    errorExit name $ "unrecognized argument '" ++ o ++ "'"
+                forM_ unrecognized $ \o ->
+                    errorExit name $ "unrecognized option '" ++ o ++ "'"
+                exitFailure
+
+instance IsCmd Group where
+    getCmdHelp = groupHelp
+    getOptDescr _ = []
+
+    getUsageHeader _ _ = " <COMMAND> [ARGS...]"
+    getUsageFooter g _ = unlines $
+        [ ""
+        , "Commands: "
+        ] ++
+        [ "  " ++ name ++ replicate (12 - length name) ' ' ++ getCmdHelp c
+        | SubCmd name c <- groupCmds g
+        ]
+
+    runCmd g name mbver _options (cmd: nonOptions) unrecognized =
+        case [ SubCmd subname c | SubCmd subname c <- groupCmds g, subname == cmd ] of
+           [SubCmd subname c] ->
+               run' c (name ++ [subname]) mbver (nonOptions ++ unrecognized)
+           _ ->
+               errorExit name $ "unrecognized command: " ++ cmd
+    runCmd _ name _ _ _ _ =
+        errorExit name "no command given"
+
+-- | Make a sub command
+subCmd :: IsCmd c => String -> c -> SubCmd
+subCmd = SubCmd
+
+-- runner
+
+run' :: IsCmd c => c -> [String] -> Maybe String -> [String] -> IO ()
+run' cmd name mbver args = do
+    let optDescr =
+            getOptDescr cmd
+            ++ [ Option "?" ["help"]    (NoArg ("help",    "t")) "display this help and exit" ]
+            ++ [ Option "V" ["version"] (NoArg ("version", "t")) "output version information and exit"
+               | isJust mbver ]
+            ++ [ Option "v" ["verbose"] (OptArg (\arg -> ("verbose", fromMaybe "" arg)) "n") "set verbosity level" ]
+
+        prog     = unwords name
+        vermsg   = prog ++ maybe "" (" version " ++) mbver
+        header = "Usage: " ++ prog ++ " [OPTION...]" ++ getUsageHeader cmd prog ++ "\n" ++
+                 "  " ++ getCmdHelp cmd ++ "\n\n" ++
+                 "Options:"
+
+        usage    =
+            usageInfo header optDescr ++
+            getUsageFooter cmd prog
+
+    case getOpt' RequireOrder optDescr args of
+        (options, nonOptions, unrecognized, errors)
+            | not $ null errors ->
+                  errorExit name $ intercalate ", " errors
+            | isJust (lookup "help" options) -> do
+                  putStr usage
+                  exitSuccess
+            | isJust (lookup "version" options) -> do
+                  putStrLn vermsg
+                  exitSuccess
+            | otherwise ->
+                  runCmd cmd name mbver options nonOptions unrecognized
+
+-- | Run a command with specifying program name and version
+run :: IsCmd c => String -> Maybe String -> c -> IO ()
+run progName progVer cmd =
+    run' cmd [progName] progVer =<< getArgs
+
+-- | Run a command
+run_ :: IsCmd c => c -> IO ()
+run_ cmd = do
+    progName <- getProgName
+    run progName Nothing cmd
+
+errorExit :: [String] -> String -> IO ()
+errorExit name msg = do
+    let prog = unwords name
+    hPutStrLn stderr $ prog ++ ": " ++ msg
+    hPutStrLn stderr $ "Try '" ++ prog ++ " --help' for more information."
+    exitFailure