$idris ____ __ _ / _/___/ /____(_)____ / // __ / ___/ / ___/ Version 0.9.12-git:dae7d7d _/ // /_/ / / / (__ ) http://www.idris-lang.org/ /___/\__,_/_/ /_/____/ Type :? for help  install $ git clone git://github.com/edwinb/Idris-dev.git idris
$cd idris$ echo 'CABALFLAGS += -f FFI -f curses' > custom.mk
$diff quine.idr <(./a.out)  haskell同様、showwhereのおかげで非常にquineが書きやすい sの型注釈が要るのは何故だ fibonacci module Main fibs : Stream Nat fibs = map fib [0..] main : IO () main = recur fibs where recur (x :: xs) = do print x recur xs  fib : Nat -> NatPreludeにあるという恐ろしさよ haskellのmapM_traverse_に吸収された 良い また、[0..]が無限長なため全域関数traverse_では扱えず、IOの中で処理せねばならない applicative style しかし、haskellでは等価な以下のような別表現は動かない main' : IO () main' = recur fibs where recur (x :: xs) = print x$> recur xs

main'' : IO ()
main'' = recur fibs where
recur (x :: xs) = print x >>= const (recur xs)


replで試すと do $> >>= それぞれ以下のような簡約結果になる Idris> do { putStrLn "hoge" ; print 3 } io_bind (MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "hoge\n" w)) (\{bindx0} => MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "3\n" w)) : IO () Idris> putStrLn "hoge"$> print 3
io_bind (io_bind (MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "hoge\n" w)) (\{b0} => io_return id))
(\f' => io_bind (MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "3\n" w)) (\a' => io_return (f' a'))) : IO ()
Idris> putStrLn "hoge" >>= const (print 3)
io_bind (MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "hoge\n" w))
(\v => MkIO (\{w0} => mkForeignPrim (FFun "putStr" [FString] FUnit) "3\n" w)) : IO ()


main''' : IO ()
main''' = recur fibs where
recur (x :: xs) = do
print x
recur xs
putStrLn "foo"


fizzbuzz

PreludeSemigroupやばい
あるからには使わねばならない

module Main

data FizzBuzz = Fizz | Buzz | Fizzbuzz

fizz : Nat -> Maybe FizzBuzz
fizz n = if (n mod 3) == 0 then Just Fizz else Nothing
buzz : Nat -> Maybe FizzBuzz
buzz n = if (n mod 5) == 0 then Just Buzz else Nothing

instance Eq FizzBuzz where
Fizzbuzz == Fizzbuzz = True
Fizz == Fizz = True
Buzz == Buzz = True
_ == _ = False

instance Semigroup FizzBuzz where
a <+> b = if a == b then a else Fizzbuzz

fizzbuzz : Nat -> Maybe FizzBuzz
fizzbuzz n = fizz n <+> buzz n

instance Show FizzBuzz where
show Fizz = "fizz"
show Buzz = "buzz"
show Fizzbuzz = "fizzbuzz"

main : IO ()
main = recur 1 where
recur : Nat -> IO ()
recur n = do
putStrLn $fromMaybe (show n) (map show$ fizzbuzz n)
recur \$ succ n


そして肝心の証明はよく分からなかったので全列挙しました

instance VerifiedSemigroup FizzBuzz where
semigroupOpIsAssociative Fizz     Fizz     Fizz     = refl
semigroupOpIsAssociative Fizz     Fizz     Buzz     = refl
semigroupOpIsAssociative Fizz     Fizz     Fizzbuzz = refl
semigroupOpIsAssociative Fizz     Buzz     Fizz     = refl
semigroupOpIsAssociative Fizz     Buzz     Buzz     = refl
semigroupOpIsAssociative Fizz     Buzz     Fizzbuzz = refl
semigroupOpIsAssociative Fizz     Fizzbuzz Fizz     = refl
semigroupOpIsAssociative Fizz     Fizzbuzz Buzz     = refl
semigroupOpIsAssociative Fizz     Fizzbuzz Fizzbuzz = refl
semigroupOpIsAssociative Buzz     Fizz     Fizz     = refl
semigroupOpIsAssociative Buzz     Fizz     Buzz     = refl
semigroupOpIsAssociative Buzz     Fizz     Fizzbuzz = refl
semigroupOpIsAssociative Buzz     Buzz     Fizz     = refl
semigroupOpIsAssociative Buzz     Buzz     Buzz     = refl
semigroupOpIsAssociative Buzz     Buzz     Fizzbuzz = refl
semigroupOpIsAssociative Buzz     Fizzbuzz Fizz     = refl
semigroupOpIsAssociative Buzz     Fizzbuzz Buzz     = refl
semigroupOpIsAssociative Buzz     Fizzbuzz Fizzbuzz = refl
semigroupOpIsAssociative Fizzbuzz Fizz     Fizz     = refl
semigroupOpIsAssociative Fizzbuzz Fizz     Buzz     = refl
semigroupOpIsAssociative Fizzbuzz Fizz     Fizzbuzz = refl
semigroupOpIsAssociative Fizzbuzz Buzz     Fizz     = refl
semigroupOpIsAssociative Fizzbuzz Buzz     Buzz     = refl
semigroupOpIsAssociative Fizzbuzz Buzz     Fizzbuzz = refl
semigroupOpIsAssociative Fizzbuzz Fizzbuzz Fizz     = refl
semigroupOpIsAssociative Fizzbuzz Fizzbuzz Buzz     = refl
semigroupOpIsAssociative Fizzbuzz Fizzbuzz Fizzbuzz = refl