Masahiro Sakai msakai

I hereby claim:

To claim this, I am signing this object:

	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	module ProximalGradientMethod where

	import Data.Foldable
	import Data.Reflection (Reifies)
	import qualified Data.Vector.Storable as V
	import Numeric.AD
	import Numeric.AD.Mode.Reverse

	{-# LANGUAGE FlexibleContexts #-}

	import Control.Exception
	import qualified Data.Vector.Generic as VG
	import Numeric.LinearAlgebra

	eulerMethod :: Fractional a => (a -> a -> a) -> a -> a -> a -> a
	eulerMethod f h t y = y + h * f t y

	-- https://ja.wikipedia.org/wiki/%E3%83%AB%E3%83%B3%E3%82%B2%EF%BC%9D%E3%82%AF%E3%83%83%E3%82%BF%E6%B3%95

	{-# LANGUAGE BangPatterns #-}

	import Control.Exception

	-- crt [(3,2), (5,3), (7,2)] == 23
	crt :: [(Integer, Integer)] -> Integer
	crt xs = assert (all (\(n, a) -> ret `mod` n == a) xs) $ ret
	where
	ret = foldl add 0 [m' `mul` a `mul` t \| (n, a) <- xs, let m' = m `div` n, let (d, t, _) = exgcd m' (- n), assert (d == 1) True]
	m = product [n \| (n, a) <- xs]

	{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}

	import Test.QuickCheck
	import qualified Test.QuickCheck.Monadic as QM
	import qualified Z3.Monad as Z3

	{-
	a x + b y = n d where d = gcd(a,b) の解は必ず
	(x, y) = (n x0 + b/d k, n y0 - a/d k)
	の形で書けることを示したい。

	{-
	https://twitter.com/andrejbauer/status/1358357606536986624

	Today's exercise in constructive math: characterize the maximal
	elements of Plotkin's domain T^ω := {(A,B) ∈ P(ℕ) × P(ℕ) \| A ∩ B = ∅},
	ordered by pairwise ⊆. Coq definitions are in the picture.
	Hint: they are not just those that satisfy A ∪ B = ℕ.
	-}
	module Tomega where

	{-# OPTIONS_GHC -Wall #-}
	module OptimalTransport (computeOptimalTransport) where

	import qualified Data.Vector.Generic as VG
	import Numeric.LinearAlgebra ((<.>), (#>), (<#), (><))
	import qualified Numeric.LinearAlgebra as LA

	-- \| Solve entropy regularized optimal transport problem:
	--
	-- \[

	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE QuantifiedConstraints #-}

	data Rose f a = Branch a (f (Rose f a))

	type Eq1 f = (forall b. Eq b => Eq (f b))
	{-
	ng.hs:6:33: error:
	• Expected a type, but ‘Eq (f b)’ has kind ‘Constraint’
	• In the type ‘(forall b. Eq b => Eq (f b))’