Skip to content

Instantly share code, notes, and snippets.

Hidenori Azuma as-capabl

Block or report user

Report or block as-capabl

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@as-capabl
as-capabl / oreore_monad.md
Created May 10, 2019
妄想C++言語拡張 - オーバーロード可能セミコロンとしてのモナド
View oreore_monad.md

言語拡張は以下の2点。

  • クラスにoperator doを定義できるようにする
  • do 型名 { 変数宣言 <- 値; 値; ...} という構文の新設

使用イメージは以下のような感じ。

// モナドの型
template <typename T> class MyMonad {
  MyMonad(const T& t) {...} // Haskellのpure(return)に相当
View Lang.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TupleSections #-}
module SLang where
import Control.Monad.State
import Data.Bool
import Data.Maybe
import Control.Monad.Trans.Iter
import Control.Monad.Identity
@as-capabl
as-capabl / kequiv.hs
Created Jul 11, 2018
Path inductionで型レベル同値関係から値レベル同値関係を導く
View kequiv.hs
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications, TypeInType, GADTs, RankNTypes #-}
import GHC.Types
import Data.Type.Equality
import Unsafe.Coerce
-- 仮定:Path Induction
indEquiv ::
forall k (t :: forall (x :: k) (y :: k). (x :~: y) -> Type).
View siri_improved.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
module Main where
@as-capabl
as-capabl / upgrade.hs
Created Aug 25, 2017
extensible-effectsの作用の拡大
View upgrade.hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
import Control.Eff
import Control.Monad.Free.Reflection
import Data.OpenUnion
import Data.Typeable
-- http://aiya000.github.io/posts/2017-08-22-my-experience-of-eff-convertion.html
View sumeven.hs
{-# LANGUAGE BangPatterns #-}
import Data.List (foldl')
-- お題:リスト中の偶数を全部足す
-- 最高
sumEven1 :: [Int] -> Int
sumEven1 = foldl' (+) 0 . filter even
-- 書いてしまいがちなクソコード
@as-capabl
as-capabl / builder.hs
Created May 10, 2017
Writerっぽくリスト作れて、遅延評価とかfoldr/buildとか効くヤツ
View builder.hs
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
as-capabl / lens-prism.hs
Created Feb 21, 2017
LensとPrismで解きたい問題
View lens-prism.hs
-- 与えるもの:あるレコード型とその上のLens
data Hoge = Hoge { _hoge1 :: ..., _hoge2 :: ..., ... }
makeLenses ''Hoge -- hoge1, hoge2, ...が定義される
-- ↓ ここからTemplate Haskellで生成するか、あるいは...
-- 欲しいもの1:直和型とその上のPrism
data CoHoge = CoHoge1 ... | CoHoge2 ...
makePrisms ''CoHoge -- _CoHoge1, _CoHoge2, ...が定義される
-- CoHogeのコンストラクタはなくてもいい。型とPrismが必要
View simplex_category.v
Require Import Relation_Definitions.
Require Import SetoidClass.
Require Import VectorDef.
Require Import Morphisms.
Require Import COC.Base.Main.
Set Implicit Arguments.
@as-capabl
as-capabl / ReaderTImpl.v
Created Jun 27, 2016
やりたいこと:Coq上でReaderTを実装し、Haskellコードに変換してHaskell側から使う
View ReaderTImpl.v
(* やりたいこと: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)
You can’t perform that action at this time.