Instantly share code, notes, and snippets.

# Icelandjack/Code.markdown

Created June 2, 2017 14:46
Star You must be signed in to star a gist
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```

# TODO

Something like

```data Exp :: Type -> Type where
I :: Int -> Exp Int
T :: Exp Bool
F :: Exp Bool
A :: Exp Int -> Exp Int -> Exp Int

class    Elem a where
instance Elem Int
instance Elem Bool

specialElimExp :: Exp a -> ((Eq a, Show a) => r) -> r
specialElimE = \case
I i ->  ...```

and then create, not only

```pattern Eval :: a -> Exp a
pattern Eval a <- (eval -> e)
where Eval a =```

gah never mind, I wanted

`pattern Eval :: (Eq a, Show a) => () => a -> Expr a`

### 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