as-capabl

{-# Language Arrows #-}

import Control.Arrow
import Control.Monad (forever)
import Control.Monad.Trans (lift)
import qualified Control.Arrow.Machine as P
import qualified Data.Machine as Mc
import Data.Machine ((<~))

as-capabl

{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}
{-# Language LambdaCase #-}

module
    Main

as-capabl

Require Import List.

Section Monoid.
  Class Monoid {A:Type} (dot : A -> A -> A) (unit : A) : Prop :=
    {
      dot_assoc :
        forall x y z:A,
          dot x (dot y z) = dot (dot x y) z;
      unit_left :
        forall x, dot unit x = x;

as-capabl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}


module
    Main
where

as-capabl

{-# LANGUAGE Arrows #-}

module Main where

import Prelude hiding (filter, id, (.), unzip, mapM_)
import Control.Category
import Control.Arrow
import Criterion
import Criterion.Main (defaultMain)
import Data.Time

as-capabl

(* やりたいこと：Coq上でReaderTを実装し、
 Haskellコードに変換してHaskell側から使う *)
Require Import Coq.Logic.FunctionalExtensionality.

Section Monad_Definition.
  (* Reserved Notation "c >>= f"
           (at level 42, left associativity). *)

  (* Monadの宣言 *)
  Class Monad {T : Type -> Type} (returns : forall {A : Type}, A -> T A)

as-capabl

Require Import Relation_Definitions.
Require Import SetoidClass.
Require Import VectorDef.
Require Import Morphisms.
Require Import COC.Base.Main.


Set Implicit Arguments.

as-capabl

-- 与えるもの：あるレコード型とその上のLens
data Hoge = Hoge { _hoge1 :: ..., _hoge2 :: ..., ... }
makeLenses ''Hoge -- hoge1, hoge2, ...が定義される

-- ↓ ここからTemplate Haskellで生成するか、あるいは...

-- 欲しいもの1：直和型とその上のPrism 
data CoHoge = CoHoge1 ... | CoHoge2 ...
makePrisms ''CoHoge -- _CoHoge1, _CoHoge2, ...が定義される
    -- CoHogeのコンストラクタはなくてもいい。型とPrismが必要

as-capabl

module Main where

import Control.Monad.Free.Church
import GHC.Exts (build)
import Control.Monad (forever)

type Builder b = F ((,) b)

putB :: b -> Builder b ()
putB x = liftF (x, ())

as-capabl

{-# LANGUAGE BangPatterns #-}
import Data.List (foldl')

-- お題：リスト中の偶数を全部足す

-- 最高
sumEven1 :: [Int] -> Int
sumEven1 = foldl' (+) 0 . filter even

-- 書いてしまいがちなクソコード