Instantly share code, notes, and snippets.

# Icelandjack/Code.markdown

Created Jun 2, 2017
TODO: Look at when on laptop

```simplify :: Expr SomePrim (Type s) a -> Either String (MP s a)
simplify (Var a)                = pure (MPApp (MPVar a))
simplify (Prim (SomePrim p))    = simplifyPrim0 p
simplify (Lam _ _)              = throwError "Non-applied lambda abstraction"
simplify (Let (TyScalar s) e b) = mpLet s <\$> simplify e <*> transverseScope simplify b
simplify (Let (_ :-> _) e b)    = simplify (instantiate1 e b)
simplify (App f x)              = case whnf f of
Lam _ b                   -> simplify (instantiate1 x b)
Prim (SomePrim p)         -> simplifyPrim1 p x
App (Prim (SomePrim p)) y -> simplifyPrim2 p y x
_                         -> throwError \$ "Non-primitive application"

-- ...

simplifyPrim2 :: forall arity s a. IArity arity
=> Prim arity
-> Expr SomePrim (Type s) a
-> Expr SomePrim (Type s) a
-> Either String (MP s a)
simplifyPrim2 p x y = case iarity :: SArity arity of
Arity0 -> throwError \$ "Application of 0-arity primitive: " ++ show p
Arity1 -> throwError \$ "Over-application of 1-arity primitive: " ++ show p
Arity2 -> (\x' y' -> floatTop (MPApp2 p (pure x') (pure y')))
<\$> simplify x
<*> simplify y```

### Icelandjack commented Jun 12, 2017 • edited

https://pdfs.semanticscholar.org/bc0d/09a0807399cf0a8f3c1f3c37063bfb45fa9f.pdf

The data type STM implements data constructors for all STM-operations, where continuations
corresponding to the `>>=`-operator for sequencing are packed into the constructors.

```data STM a = Return a
| Retry
| ∀ b. NewTVar b (TVar b → STM a)
| ∀ b. ReadTVar (TVar b) (b → STM a)
| ∀ b. WriteTVar (TVar b) b (STM a)
| ∀ b. OrElse (STM b) (STM b) (b → STM a)```

The STM-operations generate the corresponding data, and the monad instance for the type
STM is implemented straightforward, where the bind-operator `>>=` combines the actions:

```newTVar :: a → STM (TVar a) writeTVar :: TVar a → a → STM ()
newTVar a = NewTVar a return writeTVar v x = WriteTVar v x (return ())

readTVar :: TVar a → STM a

orElse :: STM a → STM a → STM a
orElse a1 a2 = OrElse a1 a2 return

retry :: STM a
retry = Retry