Experience reporting using indexed monads in production?

Question

In a previous question, I discovered the existence of Conor McBride arrows Kleisli Outrageous Fortune , looking for ways to encode Idris Examples in Haskell . My efforts to understand MacBride code and compile it in Haskell led to this point: https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f

During a search in Hackage, I discovered several implementations of these concepts, in particular (suppose, who?) Edward Kmett and Gabriel Gonzalez .

How do people produce such code in production? In particular, are the expected benefits (runtime security, self-determination) actually happening in the IRL? How about saving this kind of code over time and hosting new users?

EDIT: I changed the name to be more explicit regarding what I'm looking for: in the real world, the use of indexed monads in the wild. I am interested in using them, and I have several use cases, just wondering if other people used the "production" code.

EDIT 2: Thanks to the great answers provided so far and the helpful comments, I again edited the title and description of the question to more accurately reflect what answer I am expecting, for example. an experience.

Answer 1

I think that the following should be considered a practical example: statically applying "good fit" to the compiler. First install the boiler:

{-# LANGUAGE GADTs, KindSignatures #-} {-# LANGUAGE DataKinds, TypeOperators #-} {-# LANGUAGE RebindableSyntax #-} import qualified Prelude import Prelude hiding (return, fail, (>>=), (>>)) 

Then a simple stack language:

 data Op (i :: [*]) (j :: [*]) where IMM :: a -> Op i (a ': i) BINOP :: (a -> b -> c) -> Op (a ': b ': i) (c ': i) BRANCH :: Label ij -> Label ij -> Op (Bool ': i) j 

and we will not worry about real Label s:

 data Label (i :: [*]) (j :: [*]) where Label :: Prog ij -> Label ij 

and Prog drums are just Op s string lists:

 data Prog (i :: [*]) (j :: [*]) where PNil :: Prog ii PCons :: Op ij -> Prog jk -> Prog ik 

So, in this parameter we can very easily create a compiler, which is the monadic monad of the writer; i.e. indexed monad:

 class IMonad (m :: idx -> idx -> * -> *) where ireturn :: a -> miia ibind :: mija -> (a -> mjkb) -> mikb -- For RebindableSyntax, so that we get that sweet 'do' sugar return :: (IMonad m) => a -> miia return = ireturn (>>=) :: (IMonad m) => mija -> (a -> mjkb) -> mikb (>>=) = ibind m >> n = m >>= const n fail = error 

which allows you to accumulate (n indexed) monoid:

 class IMonoid (m :: idx -> idx -> *) where imempty :: mii imappend :: mij -> mjk -> mik 

like a regular Writer :

 newtype IWriter w (i :: [*]) (j :: [*]) (a :: *) = IWriter{ runIWriter :: (wij, a) } instance (IMonoid w) => IMonad (IWriter w) where ireturn x = IWriter (imempty, x) ibind mf = IWriter $ case runIWriter m of (w, x) -> case runIWriter (fx) of (w', y) -> (w `imappend` w', y) itell :: wij -> IWriter wij () itell w = IWriter (w, ()) 

So, we just apply this technique to Prog rams:

 instance IMonoid Prog where imempty = PNil imappend PNil prog' = prog' imappend (PCons op prog) prog' = PCons op $ imappend prog prog' type Compiler = IWriter Prog tellOp :: Op ij -> Compiler ij () tellOp op = itell $ PCons op PNil label :: Compiler ij () -> Compiler kk (Label ij) label m = case runIWriter m of (prog, ()) -> ireturn (Label prog) 

and then we can try to compose a simple expression language:

 data Expr a where Lit :: a -> Expr a And :: Expr Bool -> Expr Bool -> Expr Bool Plus :: Expr Int -> Expr Int -> Expr Int If :: Expr Bool -> Expr a -> Expr a -> Expr a compile :: Expr a -> Compiler i (a ': i) () compile (Lit x) = tellOp $ IMM x compile (And xy) = do compile x compile y tellOp $ BINOP (&&) compile (Plus xy) = do compile x compile y tellOp $ BINOP (+) compile (If bte) = do labThen <- label $ compile t labElse <- label $ compile e compile b tellOp $ BRANCH labThen labElse 

and if we omit, for example. one of the BINOP arguments, typechecker will detect this:

 compile (And xy) = do compile x tellOp $ BINOP (&&) 

• Failed to deduce: i ~ (Bool : i) from context: a ~ Bool

Answer 2

Session types are an attempt to describe layer descriptions on network protocols. The idea is that if a client sends a value, the server must be ready to receive it, and vice versa.

So here is a type (using TypeInType ) that describes sessions consisting of a sequence of values ​​to send and values ​​to receive.

 infixr 5 :!, :? data Session = Type :! Session | Type :? Session | E 

a :! s a :! s means "send a value of type a and then continue with protocol s ". a :? s a :? s means "get a value of type a and then continue with protocol s ".

So, Session is a (type-level) list of actions. Our monadic calculations will work their way up this list, sending and receiving data as needed. More specifically, evaluating the type Chan sta reduces the remaining work that must be done to satisfy the protocol from s to t . I will build Chan using the indexed free monad that I used in my answer to your other question.

 class IFunctor f where imap :: (a -> b) -> fija -> fijb class IFunctor m => IMonad m where ireturn :: a -> miia (>>>=) :: mija -> (a -> mjkb) -> mikb data IFree fija where IReturn :: a -> IFree fiia IFree :: fij (IFree fjka) -> IFree fika instance IFunctor f => IFunctor (IFree f) where imap f (IReturn x) = IReturn (fx) imap f (IFree fx) = IFree (imap (imap f) fx) instance IFunctor f => IMonad (IFree f) where ireturn = IReturn IReturn x >>>= f = fx IFree fx >>>= f = IFree (imap (>>>= f) fx) 

Our basic actions in the Chan monad will simply send and receive values.

 data ChanF str where Send :: a -> r -> ChanF (a :! s) sr Recv :: (a -> r) -> ChanF (a :? s) sr instance IFunctor ChanF where imap f (Send xr) = Send x (fr) imap f (Recv r) = Recv (fmap fr) send :: a -> Chan (a :! s) s () send x = IFree (Send x (IReturn ())) recv :: Chan (a :? s) sa recv = IFree (Recv IReturn) type Chan = IFree ChanF type Chan' s = Chan s E -- a "complete" Chan 

send takes the current session state from a :! s a :! s to s , fulfilling the obligation to send a . Similarly, recv converts the session from a :? s a :? s to s .

Here's the interesting part. When one end of the protocol sends a value, the other end must be ready to receive it, and vice versa. This leads to the idea of ​​a double session type:

 type family Dual s where Dual (a :! s) = a :? Dual s Dual (a :? s) = a :! Dual s Dual E = E 

In a common language, Dual (Dual s) = s will be provable, but alas, Haskell is not complete.

You can connect a pair of channels if their types are dual. (I think you would call it a memory simulation for connecting the client and server.)

 connect :: Chan' sa -> Chan' (Dual s) b -> (a, b) connect (IReturn x) (IReturn y) = (x, y) connect (IReturn _) (IFree y) = case y of {} connect (IFree (Send xr)) (IFree (Recv f)) = connect r (fx) connect (IFree (Recv f)) (IFree (Send yr)) = connect (fy) r 

For example, a protocol is used here for a server that checks to see if it is greater than 3. 3. The server waits for an Int , sends Bool back, and then completes the calculation.

 type MyProtocol = Int :? Bool :! E server :: Chan' MyProtocol () server = do -- using RebindableSyntax x <- recv send (x > 3) client :: Chan' (Dual MyProtocol) Bool client = do send 5 recv 

And check this out:

 ghci> connect server client ((),True) 

Session types are an area of ​​active research. This particular implementation is great for very simple protocols, but you cannot describe protocols where the type of data sent over the wire depends on the state of the protocol. To do this, you need unexpected surprises, dependent types. See this talk from Brady for a quick demonstration of the state of session types.

Answer 3

Another nice example is mutexes with a lock-unlock check at compile time. You can find this example on the Stephen Diehl website:

http://dev.stephendiehl.com/hask/#indexed-monads