Skip to content

Instantly share code, notes, and snippets.

Avatar

Masahiro Sakai msakai

View GitHub Profile
View test_associated_types.hs
{-# LANGUAGE FlexibleContexts, GADTs, TypeFamilies #-}
class T a where
type Config a
getConfig :: a -> Config a
data D where
T :: T a => a -> D
View ProximalGradientMethod.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ProximalGradientMethod where
import Data.Foldable
import Data.Reflection (Reifies)
import Numeric.AD
import Numeric.AD.Mode.Reverse
import Numeric.AD.Internal.Reverse (Tape)
View RungeKutta.hs
{-# 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
View ChineseRemainderTheorem.hs
{-# 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]
View Bezout.hs
{-# 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)
の形で書けることを示したい。
View keybase.md

Keybase proof

I hereby claim:

  • I am msakai on github.
  • I am msakai (https://keybase.io/msakai) on keybase.
  • I have a public key ASDrKkF7omBH58cR0sbmFTS_5TDhq_tjLEVi0wWi2IFfNgo

To claim this, I am signing this object:

View Tomega.agda
{-
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
View OptimalTransport.hs
{-# 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:
--
-- \[
@msakai
msakai / ng.hs
Last active Aug 4, 2020
Interaction of ConstraintKinds and QuantifiedConstraints. There was already an issue about it https://gitlab.haskell.org/ghc/ghc/-/issues/16139 .
View ng.hs
{-# 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))’