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
@msakai
msakai / umineko8challenge.als
Created Jan 10, 2011
うみねこのなく頃に8 のベルンの挑戦のAlloyモデル
View umineko8challenge.als
// うみねこのなく頃に8 のベルンの挑戦のAlloyモデル
abstract sig Person { kill : set Person }
one sig
Krauss, Natsuhi, Jessica,
Eva, Hideyoshi, George,
Rudolf, Kyrie, Battler,
Rosa, Maria,
Nanjo,
Genji, Shannon, Kanon, Gouda, Kumasawa
extends Person {}
@msakai
msakai / FlightRadar24.hs
Created Aug 10, 2012
Sample for fetching JSON data from flightradar24.com
View FlightRadar24.hs
import Control.Concurrent
import Control.Monad
import Data.Maybe
import Data.Time
import Network.Browser
import Network.HTTP
import Network.HTTP.Proxy
import Network.URI
import System.Locale
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