Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 3, 2017


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

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 12, 2017

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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment