Where does '[] come from and where is it declared?

Question

Looking at the example code from freer-simple

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
module Console where

import Control.Monad.Freer
import Control.Monad.Freer.Error
import Control.Monad.Freer.State
import Control.Monad.Freer.Writer
import System.Exit hiding (ExitCode(ExitSuccess))

--------------------------------------------------------------------------------
                                                             -- Effect Model --
--------------------------------------------------------------------------------
data Console r where
    PutStrLn    :: String -> Console ()
    GetLine     :: Console String
    ExitSuccess :: Console ()

putStrLn' :: Member Console effs => String -> Eff effs ()
putStrLn' = send . PutStrLn

getLine' :: Member Console effs => Eff effs String
getLine' = send GetLine

exitSuccess' :: Member Console effs => Eff effs ()
exitSuccess' = send ExitSuccess

--------------------------------------------------------------------------------
                                                    -- Effectful Interpreter --
--------------------------------------------------------------------------------
runConsole :: Eff '[Console, IO] a -> IO a
runConsole = runM . interpretM (\case
    PutStrLn msg -> putStrLn msg
    GetLine -> getLine
    ExitSuccess -> exitSuccess)

I don't get where the curious looking '[...] comes from in Eff '[Console, IO] a.

I get that it declares a list of Effects for the interpreter but where is it declared?

I poked around the source code of the library but couldn't see anything I recognised as a "constructor".

Is it a Haskell feature for does it come from a low level type-fu library?

What is a more rigorous description of it's purpose?

Where does '[] come from and where is it declared?

0 Answers0