@@ -0,0 +1,56 @@
1+module Main
2+
3+data Free : (f : Type -> Type) -> (a : Type) -> Type where
4+ Pure : a -> Free f a
5+ Bind : f (Free f a) -> Free f a
6+
7+Functor f => Functor (Free f) where
8+ map f m = assert_total $ case m of
9+ Pure x => Pure (f x)
10+ Bind x => Bind (map (map f) x)
11+
12+Functor f => Applicative (Free f) where
13+ pure = Pure
14+
15+ m <*> x = assert_total $ case m of
16+ Pure f => map f x
17+ Bind f => Bind (map (<*> x) f)
18+
19+Functor f => Monad (Free f) where
20+ m >>= f = assert_total $ case m of
21+ Pure x => f x
22+ Bind x => Bind (map (>>= f) x)
23+
24+liftFree : Functor f => f a -> Free f a
25+liftFree = assert_total $ Bind . map Pure
26+
27+foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
28+foldFree f m = assert_total $ case m of
29+ Pure x => pure x
30+ Bind x => f x >>= foldFree f
31+
32+data FileSystemF next
33+ = ReadFile (String -> next)
34+
35+FileSystem : Type -> Type
36+FileSystem = Free FileSystemF
37+
38+Functor FileSystemF where
39+ map f (ReadFile nextFn) = ReadFile (f . nextFn)
40+
41+readFileF : FileSystem String
42+readFileF = liftFree $ ReadFile id
43+
44+
45+
46+interpret2 : FileSystemF a -> IO a
47+interpret2 (ReadFile nextFn) = do
48+ contents <- pure "ola"
49+ pure (nextFn contents)
50+
51+main : IO ()
52+main =
53+ do
54+ c <- foldFree interpret2 readFileF
55+ putStrLn' c
56+