{{ message }}

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

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

 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 readTVar a = ReadTVar a return orElse :: STM a → STM a → STM a orElse a1 a2 = OrElse a1 a2 return retry :: STM a retry = Retry instance Monad STM where return = Return m >>= f = case m of Return x → f x Retry → Retry NewTVar x ct → NewTVar x (λi → ct >>= f) ReadTVar x ct → ReadTVar x (λi → ct >>= f) WriteTVar v x ct → WriteTVar v x (ct >>= f) OrElse a1 a2 ct → OrElse a1 a2 (λi → ct >>= f)```