DeepDarkFantasy 0.0.1.1 → 0.2017.3.28

raw patch · 8 files changed

+666/−571 lines, 8 filesdep +constraintsPVP ok

version bump matches the API change (PVP)

Dependencies added: constraints

API changes (from Hackage documentation)

Files

• DeepDarkFantasy.cabal +5/−6
• src/Comb.hs +0/−47
• src/DBI.hs +83/−415
• src/HOAS.hs +0/−35
• src/Lang.hs +543/−0
• src/Main.hs +0/−19
• src/Poly.lhs +5/−4
• src/Xor.lhs +30/−45

@@ -1,5 +1,5 @@ name: DeepDarkFantasy-version: 0.0.1.1+version: 0.2017.3.28 cabal-version: 1.12 build-type: Simple license: Apache@@ -16,17 +16,16 @@  library   exposed-modules:-    Comb     DBI-    HOAS-    Main     Poly     Xor     Util+    Lang   build-depends:     base >= 4.9.0.0 && <= 4.9.1.0,     mtl -any,-    random -any+    random -any,+    constraints -any   default-language: Haskell2010   hs-source-dirs: src-  ghc-options: -ferror-spans+  ghc-options: -ferror-spans 

@@ -1,47 +0,0 @@-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    MonomorphismRestriction #-}
-
-module Comb where
-
-class Comb repr where
-  app :: repr (a -> b) -> repr a -> repr b
-  s :: repr ((a -> b -> c) -> (a -> b) -> (a -> c))
-  k :: repr (a -> b -> a)
-  i :: repr (a -> a)
-  b :: repr ((b -> c) -> (a -> b) -> (a -> c))
-  c :: repr ((a -> b -> c) -> (b -> a -> c))
-  w :: repr ((a -> a -> b) -> (a -> b))
-
-newtype Eval x = Eval {unEval :: x}
-
-instance Comb Eval where
-  app (Eval f) (Eval x) = Eval (f x)
-  s = Eval (\f x arg -> f arg $ x arg)
-  k = Eval const
-  i = Eval id
-  b = Eval (.)
-  c = Eval flip
-  w = Eval (\f x -> f x x)
-
-newtype SShow x = SShow {unSShow :: String}
-
-instance Comb SShow where
-  app (SShow f) (SShow x) = SShow $ "(" ++ f ++ " " ++ x ++ ")"
-  s = SShow "s"
-  k = SShow "k"
-  i = SShow "i"
-  b = SShow "b"
-  c = SShow "c"
-  w = SShow "w"
-
-main :: IO ()
-main = return ()

@@ -10,26 +10,39 @@     NoMonomorphismRestriction,
     TypeFamilies,
     LiberalTypeSynonyms,
-    EmptyCase,
     FunctionalDependencies,
     ExistentialQuantification,
     InstanceSigs,
-    AllowAmbiguousTypes,
     TupleSections,
-    ConstraintKinds #-}
+    ConstraintKinds,
+    DefaultSignatures,
+    UndecidableSuperClasses,
+    TypeOperators,
+    TypeApplications,
+    PartialTypeSignatures #-}
 
 module DBI where
 import qualified Prelude as P
 import Prelude (($), (.), (+), (-), (++), show, (>>=), (*), (/), undefined)
 import Util
-import Data.Void
 import Control.Monad (when)
-import qualified Control.Monad.Writer as P
-import qualified Data.Functor.Identity as P
-import qualified Data.Tuple as P
 import System.Random
 import Data.Proxy
+import Data.Constraint
+import Data.Constraint.Forall
 
+class Monoid r m where
+  zero :: r h m
+  plus :: r h (m -> m -> m)
+
+class Monoid repr w => WithDiff repr w where
+  withDiff :: repr h ((w -> x) -> w -> Diff x w)
+
+withDiff1 = app withDiff
+
+selfWithDiff :: (DBI repr, WithDiff repr w) => repr h (w -> Diff w w)
+selfWithDiff = withDiff1 id
+
 instance Random () where
   random = ((),)
   randomR _ = random
@@ -44,227 +57,56 @@       (l, g1) = randomR (llo, lhi) g0
       (r, g2) = randomR (rlo, rhi) g1
 
-class Reify repr x where
-  reify :: x -> repr h x
-
-instance DBI repr => Reify repr () where
-  reify _ = unit
-
-instance DBI repr => Reify repr P.Double where
-  reify = lit
-
-instance (DBI repr, Reify repr l, Reify repr r) => Reify repr (l, r) where
-  reify (l, r) = mkProd2 (reify l) (reify r)
-
 class DBI repr where
   z :: repr (a, h) a
   s :: repr h b -> repr (a, h) b
-  lam :: repr (a, h) b -> repr h (a -> b)
+  abs :: repr (a, h) b -> repr h (a -> b)
   app :: repr h (a -> b) -> repr h a -> repr h b
-  mkProd :: repr h (a -> b -> (a, b))
-  zro :: repr h ((a, b) -> a)
-  fst :: repr h ((a, b) -> b)
-  lit :: P.Double -> repr h P.Double
-  litZero :: repr h P.Double
-  litZero = lit 0
-  litOne :: repr h P.Double
-  litOne = lit 1
-  doublePlus :: repr h (P.Double -> P.Double -> P.Double)
-  doubleMinus :: repr h (P.Double -> P.Double -> P.Double)
-  doubleMult :: repr h (P.Double -> P.Double -> P.Double)
-  doubleDivide :: repr h (P.Double -> P.Double -> P.Double)
   hoas :: (repr (a, h) a -> repr (a, h) b) -> repr h (a -> b)
-  hoas f = lam $ f z
-  fix :: repr h ((a -> a) -> a)
-  left :: repr h (a -> P.Either a b)
-  right :: repr h (b -> P.Either a b)
-  sumMatch :: repr h ((a -> c) -> (b -> c) -> P.Either a b -> c)
-  unit :: repr h ()
-  exfalso :: repr h (Void -> a)
-  nothing :: repr h (P.Maybe a)
-  just :: repr h (a -> P.Maybe a)
-  optionMatch :: repr h (b -> (a -> b) -> P.Maybe a -> b)
-  ioRet :: repr h (a -> P.IO a)
-  ioBind :: repr h (P.IO a -> (a -> P.IO b) -> P.IO b)
-  ioMap :: repr h ((a -> b) -> P.IO a -> P.IO b)
-  nil :: repr h [a]
-  cons :: repr h (a -> [a] -> [a])
-  listMatch :: repr h (b -> (a -> [a] -> b) -> [a] -> b)
+  hoas f = abs $ f z
   com :: repr h ((b -> c) -> (a -> b) -> (a -> c))
-  com = hlam3 $ \f g x -> app f (app g x)
-  listAppend :: repr h ([a] -> [a] -> [a])
-  listAppend = hlam2 $ \l r -> fix2 (hlam $ \self -> listMatch2 r (hlam2 $ \a as -> cons2 a (app self as))) l
-  writer :: repr h ((a, w) -> P.Writer w a)
-  runWriter :: repr h (P.Writer w a -> (a, w))
-  swap :: repr h ((l, r) -> (r, l))
-  swap = hlam $ \p -> mkProd2 (fst1 p) (zro1 p)
+  com = lam3 $ \f g x -> app f (app g x)
   flip :: repr h ((a -> b -> c) -> (b -> a -> c))
-  flip = hlam3 $ \f b a -> app2 f a b
+  flip = lam3 $ \f b a -> app2 f a b
   id :: repr h (a -> a)
-  id = hlam $ \x -> x
+  id = lam $ \x -> x
   const :: repr h (a -> b -> a)
-  const = hlam2 $ \x _ -> x
+  const = lam2 $ \x _ -> x
   scomb :: repr h ((a -> b -> c) -> (a -> b) -> (a -> c))
-  scomb = hlam3 $ \f x arg -> app (app f arg) (app x arg)
-  exp :: repr h (P.Double -> P.Double)
-  curry :: repr h (((a, b) -> c) -> (a -> b -> c))
-  uncurry :: repr h ((a -> b -> c) -> ((a, b) -> c))
-  curry = hlam3 $ \f a b -> app f (mkProd2 a b)
-  uncurry = hlam2 $ \f p -> app2 f (zro1 p) (fst1 p)
+  scomb = lam3 $ \f x arg -> app2 f arg (app x arg)
+  dup :: repr h ((a -> a -> b) -> (a -> b))
+  dup = lam2 $ \f x -> app2 f x x
 
 const1 = app const
-cons2 = app2 cons
-listMatch2 = app2 listMatch
-fix1 = app fix
-fix2 = app2 fix
-uncurry1 = app uncurry
-
-class Monoid r m where
-  zero :: r h m
-  plus :: r h (m -> m -> m)
-
-class (DBI r, Monoid r g) => Group r g where
-  invert :: r h (g -> g)
-  minus :: r h (g -> g -> g)
-  invert = minus1 zero
-  minus = hlam2 $ \x y -> plus2 x (invert1 y)
-  {-# MINIMAL (invert | minus) #-}
-
-minus1 = app minus
-divide1 = app divide
-
-recip = divide1 litOne
-recip1 = app recip
-
-class Group r v => Vector r v where
-  mult :: r h (P.Double -> v -> v)
-  divide :: r h (v -> P.Double -> v)
-  mult = hlam2 $ \x y -> divide2 y (recip1 x)
-  divide = hlam2 $ \x y -> mult2 (recip1 y) x
-  {-# MINIMAL (mult | divide) #-}
-
-instance DBI r => Monoid r () where
-  zero = unit
-  plus = const1 $ const1 unit
-
-instance DBI r => Group r () where
-  invert = const1 unit
-  minus = const1 $ const1 unit
-
-instance DBI r => Vector r () where
-  mult = const1 $ const1 unit
-  divide = const1 $ const1 unit
-
-instance DBI r => Monoid r P.Double where
-  zero = litZero
-  plus = doublePlus
-
-instance DBI r => Group r P.Double where
-  minus = doubleMinus
-
-instance DBI r => Vector r P.Double where
-  mult = doubleMult
-  divide = doubleDivide
-
-instance (DBI repr, Monoid repr l, Monoid repr r) => Monoid repr (l, r) where
-  zero = mkProd2 zero zero
-  plus = hlam2 $ \l r -> mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-
-instance (DBI repr, Group repr l, Group repr r) => Group repr (l, r) where
-  invert = bimap2 invert invert
-
-instance (DBI repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
-  mult = hlam $ \x -> bimap2 (mult1 x) (mult1 x)
-
-instance (DBI repr, Monoid repr l, Monoid repr r) => Monoid repr (l -> r) where
-  zero = const1 zero
-  plus = hlam3 $ \l r x -> plus2 (app l x) (app r x)
-
-instance (DBI repr, Group repr l, Group repr r) => Group repr (l -> r) where
-  invert = hlam2 $ \l x -> app l (invert1 x)
-
-instance (DBI repr, Vector repr l, Vector repr r) => Vector repr (l -> r) where
-  mult = hlam3 $ \l r x -> app r (mult2 l x)
-
-instance DBI r => Monoid r [a] where
-  zero = nil
-  plus = listAppend
+map2 = app2 map
+return = pure
+bind2 = app2 bind
+map1 = app map
+join1 = app join
+bimap2 = app2 bimap
+flip1 = app flip
+flip2 = app2 flip
 
 class Functor r f where
   map :: r h ((a -> b) -> (f a -> f b))
 
-instance DBI r => Functor r [] where
-  map = hlam $ \f -> fix1 $ hlam $ \self -> listMatch2 nil (hlam2 $ \x xs -> cons2 (app f x) $ app self xs)
-
-map2 = app2 map
-
 class Functor r a => Applicative r a where
   pure :: r h (x -> a x)
   ap :: r h (a (x -> y) -> a x -> a y)
 
-return = pure
-
 class (DBI r, Applicative r m) => Monad r m where
   bind :: r h (m a -> (a -> m b) -> m b)
   join :: r h (m (m a) -> m a)
-  join = hlam $ \m -> bind2 m id
-  bind = hlam2 $ \m f -> join1 (app2 map f m)
+  join = lam $ \m -> bind2 m id
+  bind = lam2 $ \m f -> join1 (app2 map f m)
   {-# MINIMAL (join | bind) #-}
 
-bind2 = app2 bind
-map1 = app map
-join1 = app join
-bimap2 = app2 bimap
-flip1 = app flip
-flip2 = app2 flip
-
-class DBI r => BiFunctor r p where
+class BiFunctor r p where
   bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d)
 
-instance DBI r => BiFunctor r (,) where
-  bimap = hlam3 $ \l r p -> mkProd2 (app l (zro1 p)) (app r (fst1 p))
-
-instance DBI r => Functor r (P.Writer w) where
-  map = hlam $ \f -> com2 writer (com2 (bimap2 f id) runWriter)
-
-writer1 = app writer
-runWriter1 = app runWriter
-
-instance (DBI r, Monoid r w) => Applicative r (P.Writer w) where
-  pure = com2 writer (flip2 mkProd zero)
-  ap = hlam2 $ \f x -> writer1 (mkProd2 (app (zro1 (runWriter1 f)) (zro1 (runWriter1 x))) (plus2 (fst1 (runWriter1 f)) (fst1 (runWriter1 x))))
-
-instance (DBI r, Monoid r w) => Monad r (P.Writer w) where
-  join = hlam $ \x -> writer1 $ mkProd2 (zro1 $ runWriter1 $ zro1 $ runWriter1 x) (plus2 (fst1 $ runWriter1 $ zro1 $ runWriter1 x) (fst1 $ runWriter1 x))
-
-instance DBI r => Functor r P.IO where
-  map = ioMap
-
-ioBind2 = app2 ioBind
-
-instance DBI r => Applicative r P.IO where
-  pure = ioRet
-  ap = hlam2 $ \f x -> ioBind2 f (flip2 ioMap x)
-
-instance DBI r => Monad r P.IO where
-  bind = ioBind
-
 app3 f x y z = app (app2 f x y) z
-
-optionMatch2 = app2 optionMatch
-optionMatch3 = app3 optionMatch
 com2 = app2 com
 
-instance DBI r => Functor r P.Maybe where
-  map = hlam $ \func -> optionMatch2 nothing (com2 just func)
-
-instance DBI r => Applicative r P.Maybe where
-  pure = just
-  ap = optionMatch2 (const1 nothing) map
-
-instance DBI r => Monad r P.Maybe where
-  bind = hlam2 $ \x func -> optionMatch3 nothing func x
-
 newtype Eval h x = Eval {runEval :: h -> x}
 
 comb = Eval . P.const
@@ -272,41 +114,8 @@ instance DBI Eval where
   z = Eval P.fst
   s (Eval a) = Eval $ a . P.snd
-  lam (Eval f) = Eval $ \a h -> f (h, a)
+  abs (Eval f) = Eval $ \a h -> f (h, a)
   app (Eval f) (Eval x) = Eval $ \h -> f h $ x h
-  zro = comb P.fst
-  fst = comb P.snd
-  mkProd = comb (,)
-  lit = comb
-  doublePlus = comb (+)
-  doubleMinus = comb (-)
-  doubleMult = comb (*)
-  doubleDivide = comb (/)
-  fix = comb loop
-    where loop x = x $ loop x
-  left = comb P.Left
-  right = comb P.Right
-  sumMatch = comb $ \l r -> \case
-                             P.Left x -> l x
-                             P.Right x -> r x
-  unit = comb ()
-  exfalso = comb absurd
-  nothing = comb P.Nothing
-  just = comb P.Just
-  ioRet = comb P.return
-  ioBind = comb (>>=)
-  nil = comb []
-  cons = comb (:)
-  listMatch = comb $ \l r -> \case
-                            [] -> l
-                            x:xs -> r x xs
-  optionMatch = comb $ \l r -> \case
-                              P.Nothing -> l
-                              P.Just x -> r x
-  ioMap = comb P.fmap
-  writer = comb (P.WriterT . P.Identity)
-  runWriter = comb P.runWriter
-  exp = comb P.exp
 
 data AST = Leaf P.String | App P.String AST [AST] | Lam P.String [P.String] AST
 
@@ -321,139 +130,64 @@   show (Leaf f) = f
   show (App f x l) = "(" ++ f ++ " " ++ show x ++ P.concatMap ((" " ++) . show) l ++ ")"
   show (Lam s l t) = "(\\" ++ s ++ P.concatMap (" " ++) l ++ " -> " ++ show t ++ ")"
+
 newtype Show h a = Show {runShow :: [P.String] -> P.Int -> AST}
 name = Show . P.const . P.const . Leaf
 
 instance DBI Show where
   z = Show $ P.const $ Leaf . show . P.flip (-) 1
   s (Show v) = Show $ \vars -> v vars . P.flip (-) 1
-  lam (Show f) = Show $ \vars x -> lamAST (show x) (f vars (x + 1))
+  abs (Show f) = Show $ \vars x -> lamAST (show x) (f vars (x + 1))
   app (Show f) (Show x) = Show $ \vars h -> appAST (f vars h) (x vars h)
   hoas f = Show $ \(v:vars) h ->
     lamAST v (runShow (f $ Show $ P.const $ P.const $ Leaf v) vars (h + 1))
-  mkProd = name "mkProd"
-  zro = name "zro"
-  fst = name "fst"
-  lit = name . show
-  doublePlus = name "plus"
-  doubleMinus = name "minus"
-  doubleMult = name "mult"
-  doubleDivide = name "divide"
-  fix = name "fix"
-  left = name "left"
-  right = name "right"
-  sumMatch = name "sumMatch"
-  unit = name "unit"
-  exfalso = name "exfalso"
-  nothing = name "nothing"
-  just = name "just"
-  ioRet = name "ioRet"
-  ioBind = name "ioBind"
-  nil = name "nil"
-  cons = name "cons"
-  listMatch = name "listMatch"
-  optionMatch = name "optionMatch"
-  ioMap = name "ioMap"
-  writer = name "writer"
-  runWriter = name "runWriter"
-  exp = name "exp"
 
 class NT repr l r where
     conv :: repr l t -> repr r t
 
-instance {-# INCOHERENT #-} (DBI repr, NT repr l r) => NT repr l (a, r) where
-    conv = s . conv
+class NTS repr l r where
+    convS :: repr l t -> repr r t
 
-instance NT repr x x where
+instance (DBI repr, NT repr l r) => NTS repr l (a, r) where
+    convS = s . conv
+
+instance {-# OVERLAPPABLE #-} NTS repr l r => NT repr l r where
+    conv = convS
+
+instance {-# OVERLAPPING #-} NT repr x x where
     conv = P.id
 
-hlam :: forall repr a b h. DBI repr =>
+lam :: forall repr a b h. DBI repr =>
   ((forall k. NT repr (a, h) k => repr k a) -> (repr (a, h)) b) -> repr h (a -> b)
-hlam f = hoas (\x -> f $ conv x)
+lam f = hoas (\x -> f $ conv x)
 
-hlam2 :: forall repr a b c h. DBI repr =>
+lam2 :: forall repr a b c h. DBI repr =>
   ((forall k. NT repr (a, h) k => repr k a) -> (forall k. NT repr (b, (a, h)) k => repr k b) -> (repr (b, (a, h))) c) -> repr h (a -> b -> c)
-hlam2 f = hlam $ \x -> hlam $ \y -> f x y
+lam2 f = lam $ \x -> lam $ \y -> f x y
 
-hlam3 f = hlam2 $ \x y -> hlam $ \z -> f x y z
+lam3 f = lam2 $ \x y -> lam $ \z -> f x y z
 
 type family Diff v x
-type instance Diff v P.Double = (P.Double, v)
 type instance Diff v () = ()
-type instance Diff v (a, b) = (Diff v a, Diff v b)
 type instance Diff v (a -> b) = Diff v a -> Diff v b
-type instance Diff v (P.Either a b) = P.Either (Diff v a) (Diff v b)
-type instance Diff v Void = Void
-type instance Diff v (P.Maybe a) = P.Maybe (Diff v a)
-type instance Diff v (P.IO a) = P.IO (Diff v a)
-type instance Diff v [a] = [Diff v a]
-type instance Diff v (P.Writer w a) = P.Writer (Diff v w) (Diff v a)
+type instance Diff v (a, b) = (Diff v a, Diff v b)
 
 newtype WDiff repr v h x = WDiff {runWDiff :: repr (Diff v h) (Diff v x)}
 
 app2 f a = app (app f a)
 
-mkProd1 = app mkProd
-mkProd2 = app2 mkProd
 plus2 = app2 plus
-zro1 = app zro
-fst1 = app fst
-minus2 = app2 minus
-mult1 = app mult
-mult2 = app2 mult
-divide2 = app2 divide
-invert1 = app invert
 
-instance (Vector repr v, DBI repr) => DBI (WDiff repr v) where
+instance DBI repr => DBI (WDiff repr v) where
   z = WDiff z
   s (WDiff x) = WDiff $ s x
-  lam (WDiff f) = WDiff $ lam f
+  abs (WDiff f) = WDiff $ abs f
   app (WDiff f) (WDiff x) = WDiff $ app f x
-  mkProd = WDiff mkProd
-  zro = WDiff zro
-  fst = WDiff fst
-  lit x = WDiff $ mkProd2 (lit x) zero
-  doublePlus = WDiff $ hlam2 $ \l r ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-  doubleMinus = WDiff $ hlam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
-  doubleMult = WDiff $ hlam2 $ \l r ->
-    mkProd2 (mult2 (zro1 l) (zro1 r))
-      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))
-  doubleDivide = WDiff $ hlam2 $ \l r ->
-    mkProd2 (divide2 (zro1 l) (zro1 r))
-      (divide2 (minus2 (mult2 (zro1 r) (fst1 l)) (mult2 (zro1 l) (fst1 r)))
-        (mult2 (zro1 r) (zro1 r)))
   hoas f = WDiff $ hoas (runWDiff . f . WDiff)
-  fix = WDiff fix
-  left = WDiff left
-  right = WDiff right
-  sumMatch = WDiff sumMatch
-  unit = WDiff unit
-  exfalso = WDiff exfalso
-  nothing = WDiff nothing
-  just = WDiff just
-  ioRet = WDiff ioRet
-  ioBind = WDiff ioBind
-  nil = WDiff nil
-  cons = WDiff cons
-  listMatch = WDiff listMatch
-  optionMatch = WDiff optionMatch
-  ioMap = WDiff ioMap
-  writer = WDiff writer
-  runWriter = WDiff runWriter
-  exp = WDiff $ hlam $ \x -> mkProd2 (exp1 (zro1 x)) (mult2 (exp1 (zro1 x)) (fst1 x))
 
-exp1 = app exp
-
 noEnv :: repr () x -> repr () x
 noEnv = P.id
 
-selfWithDiff :: (DBI repr, Weight repr w) => repr h (w -> Diff w w)
-selfWithDiff = withDiff1 id
-
-withDiff1 = app withDiff
-
 class RandRange w where
   randRange :: (P.Double, P.Double) -> (w, w)
 
@@ -469,100 +203,34 @@       (llo, lhi) = randRange (lo, hi)
       (rlo, rhi) = randRange (lo, hi)
 
-instance DBI repr => Weight repr () where
-  withDiff = const1 id
-  fromDiff _ = id
+instance Weight () where weightCon = Sub Dict
 
-instance DBI repr => Weight repr P.Double where
-  withDiff = hlam2 $ \conv d -> mkProd2 d (app conv litOne)
-  fromDiff _ = zro
+instance Weight P.Double where weightCon = Sub Dict
 
-instance (DBI repr, Weight repr l, Weight repr r) => Weight repr (l, r) where
-  withDiff = hlam $ \conv -> bimap2 (withDiff1 (hlam $ \l -> app conv (mkProd2 l zero))) (withDiff1 (hlam $ \r -> app conv (mkProd2 zero r)))
-  fromDiff p = bimap2 (fromDiff p) (fromDiff p)
+instance (Weight l, Weight r) => Weight (l, r) where
+  weightCon :: forall con. (con (), con P.Double, ForallV (ProdCon con)) :- con (l, r)
+  weightCon = Sub (mapDict (prodCon \\ (instV :: (ForallV (ProdCon con) :- ProdCon con l r))) (Dict \\ weightCon @l @con \\ weightCon @r @con))
 
-class (Random w, RandRange w, Reify repr w, P.Show w, Vector repr w) => Weight repr w where
-  withDiff :: repr h ((w -> x) -> w -> Diff x w)
-  fromDiff :: Proxy x -> repr h (Diff x w -> w)
+class ProdCon con l r where
+  prodCon :: (con l, con r) :- con (l, r)
 
-data RunImpW repr h x = forall w. Weight repr w => RunImpW (repr h (w -> x))
-data ImpW repr h x = NoImpW (repr h x) | forall w. Weight repr w => ImpW (repr h (w -> x))
+instance ProdCon Random l r where prodCon = Sub Dict
 
-runImpW :: forall repr h x. DBI repr => ImpW repr h x -> RunImpW repr h x
-runImpW (ImpW x) = RunImpW x
-runImpW (NoImpW x) = RunImpW (const1 x :: repr h (() -> x))
+instance ProdCon RandRange l r where prodCon = Sub Dict
 
-data Term con h x = Term (forall r. con r => r h x)
+instance ProdCon P.Show l r where prodCon = Sub Dict
 
-instance DBI repr => DBI (ImpW repr) where
-  nil = NoImpW nil
-  cons = NoImpW cons
-  listMatch = NoImpW listMatch
-  zro = NoImpW zro
-  fst = NoImpW fst
-  mkProd = NoImpW mkProd
-  ioRet = NoImpW ioRet
-  ioMap = NoImpW ioMap
-  ioBind = NoImpW ioBind
-  unit = NoImpW unit
-  nothing = NoImpW nothing
-  just = NoImpW just
-  optionMatch = NoImpW optionMatch
-  exfalso = NoImpW exfalso
-  doublePlus = NoImpW doublePlus
-  doubleMinus = NoImpW doubleMinus
-  doubleMult = NoImpW doubleMult
-  doubleDivide = NoImpW doubleDivide
-  fix = NoImpW fix
-  left = NoImpW left
-  right = NoImpW right
-  sumMatch = NoImpW sumMatch
-  lit = NoImpW . lit
-  writer = NoImpW writer
-  runWriter = NoImpW runWriter
-  z = NoImpW z
-  s :: forall a h b. ImpW repr h b -> ImpW repr (a, h) b
-  s (ImpW x) = work x
-    where
-      work :: Weight repr w => repr h (w -> b) -> ImpW repr (a, h) b
-      work x = ImpW (s x)
-  s (NoImpW x) = NoImpW (s x)
-  app (ImpW f) (ImpW x) = ImpW (hlam $ \p -> app (app (conv f) (zro1 p)) (app (conv x) (fst1 p)))
-  app (NoImpW f) (NoImpW x) = NoImpW (app f x)
-  app (ImpW f) (NoImpW x) = ImpW (hlam $ \w -> app2 (conv f) w (conv x))
-  app (NoImpW f) (ImpW x) = ImpW (hlam $ \w -> app (conv f) (app (conv x) w))
-  lam (ImpW f) = ImpW (flip1 $ lam f)
-  lam (NoImpW x) = NoImpW (lam x)
-  exp = NoImpW exp
+class Weight w where
+  weightCon :: (con (), con P.Double, ForallV (ProdCon con)) :- con w
 
-instance DBI (Term DBI) where
-  z = Term z
-  s (Term x) = Term (s x)
-  lam (Term x) = Term (lam x)
-  app (Term f) (Term x) = Term $ app f x
-  mkProd = Term mkProd
-  zro = Term zro
-  fst = Term fst
-  lit x = Term $ lit x
-  doublePlus = Term doublePlus
-  doubleMinus = Term doubleMinus
-  doubleMult = Term doubleMult
-  doubleDivide = Term doubleDivide
-  fix = Term fix
-  left = Term left
-  right = Term right
-  sumMatch = Term sumMatch
-  unit = Term unit
-  exfalso = Term exfalso
-  nothing = Term nothing
-  just = Term just
-  optionMatch = Term optionMatch
-  exp = Term exp
-  ioRet = Term ioRet
-  ioMap = Term ioMap
-  ioBind = Term ioBind
-  nil = Term nil
-  cons = Term cons
-  listMatch = Term listMatch
-  writer = Term writer
-  runWriter = Term runWriter+data RunImpW repr h x = forall w. Weight w => RunImpW (repr h (w -> x))
+data ImpW repr h x = NoImpW (repr h x) | forall w. Weight w => ImpW (repr h (w -> x))
+
+data Combine l r h x = Combine (l h x) (r h x)
+
+instance (DBI l, DBI r) => DBI (Combine l r) where
+  z = Combine z z
+  s (Combine l r) = Combine (s l) (s r)
+  app (Combine fl fr) (Combine xl xr) = Combine (app fl xl) (app fr xr)
+  abs (Combine l r) = Combine (abs l) (abs r)
+  hoas f = Combine (hoas $ \x -> case f (Combine x z) of Combine l r -> l) (hoas $ \x -> case f (Combine z x) of Combine l r -> r)

@@ -1,35 +0,0 @@-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    MonomorphismRestriction #-}
-
-module HOAS where
-import Util
-
-class HOAS repr where
-  app :: repr (a -> b) -> repr a -> repr b
-  lam :: (repr a -> repr b) -> repr (a -> b)
-
-newtype Eval x = Eval {unEval :: x}
-
-instance HOAS Eval where
-  app (Eval f) (Eval x) = Eval (f x)
-  lam f = Eval (unEval . f . Eval)
-
-newtype HShow x = HShow {unHShow :: [String] -> String}
-
-instance HOAS HShow where
-  app (HShow f) (HShow x) = HShow (\vars -> "(" ++ f vars ++ " " ++ x vars ++ ")")
-  lam f = HShow (\(v:vars) -> "(\\" ++ v ++ " -> " ++ (unHShow $ f $ HShow $ const v) vars ++ ")")
-
-s = lam (\f -> lam (\x -> lam (\arg -> app (app f arg) (app x arg))))
-
-main :: IO ()
-main = putStrLn ((unHShow s) $ vars)

@@ -0,0 +1,543 @@+{-# LANGUAGE+    MultiParamTypeClasses,+    RankNTypes,+    ScopedTypeVariables,+    FlexibleInstances,+    FlexibleContexts,+    UndecidableInstances,+    PolyKinds,+    LambdaCase,+    NoMonomorphismRestriction,+    TypeFamilies,+    LiberalTypeSynonyms,+    FunctionalDependencies,+    ExistentialQuantification,+    InstanceSigs,+    TupleSections,+    ConstraintKinds,+    DefaultSignatures,+    UndecidableSuperClasses,+    TypeOperators,+    TypeApplications,+    PartialTypeSignatures #-}++module Lang where+import DBI+import qualified Prelude as P+import Prelude (($), (.), (+), (-), (++), show, (>>=), (*), (/), undefined)+import qualified Control.Monad.Writer as P+import qualified Data.Functor.Identity as P+import qualified GHC.Float as P+import qualified Data.Tuple as P+import Data.Void+import Data.Proxy+import Data.Proxy+import Data.Constraint+import Data.Constraint.Forall++type instance Diff v (P.Writer w a) = P.Writer (Diff v w) (Diff v a)+type instance Diff v Void = Void+type instance Diff v P.Double = (P.Double, v)+type instance Diff v P.Float = (P.Float, v)+type instance Diff v (P.Either a b) = P.Either (Diff v a) (Diff v b)+type instance Diff v (P.Maybe a) = P.Maybe (Diff v a)+type instance Diff v (P.IO a) = P.IO (Diff v a)+type instance Diff v [a] = [Diff v a]++class DBI repr => Lang repr where+  mkProd :: repr h (a -> b -> (a, b))+  zro :: repr h ((a, b) -> a)+  fst :: repr h ((a, b) -> b)+  double :: P.Double -> repr h P.Double+  doubleZero :: repr h P.Double+  doubleZero = double 0+  doubleOne :: repr h P.Double+  doubleOne = double 1+  doublePlus :: repr h (P.Double -> P.Double -> P.Double)+  doubleMinus :: repr h (P.Double -> P.Double -> P.Double)+  doubleMult :: repr h (P.Double -> P.Double -> P.Double)+  doubleDivide :: repr h (P.Double -> P.Double -> P.Double)+  doubleExp :: repr h (P.Double -> P.Double)+  float :: P.Float -> repr h P.Float+  floatZero :: repr h P.Float+  floatZero = float 0+  floatOne :: repr h P.Float+  floatOne = float 1+  floatPlus :: repr h (P.Float -> P.Float -> P.Float)+  floatMinus :: repr h (P.Float -> P.Float -> P.Float)+  floatMult :: repr h (P.Float -> P.Float -> P.Float)+  floatDivide :: repr h (P.Float -> P.Float -> P.Float)+  floatExp :: repr h (P.Float -> P.Float)+  fix :: repr h ((a -> a) -> a)+  left :: repr h (a -> P.Either a b)+  right :: repr h (b -> P.Either a b)+  sumMatch :: repr h ((a -> c) -> (b -> c) -> P.Either a b -> c)+  unit :: repr h ()+  exfalso :: repr h (Void -> a)+  nothing :: repr h (P.Maybe a)+  just :: repr h (a -> P.Maybe a)+  optionMatch :: repr h (b -> (a -> b) -> P.Maybe a -> b)+  ioRet :: repr h (a -> P.IO a)+  ioBind :: repr h (P.IO a -> (a -> P.IO b) -> P.IO b)+  ioMap :: repr h ((a -> b) -> P.IO a -> P.IO b)+  nil :: repr h [a]+  cons :: repr h (a -> [a] -> [a])+  listMatch :: repr h (b -> (a -> [a] -> b) -> [a] -> b)+  listAppend :: repr h ([a] -> [a] -> [a])+  listAppend = lam2 $ \l r -> fix2 (lam $ \self -> listMatch2 r (lam2 $ \a as -> cons2 a (app self as))) l+  writer :: repr h ((a, w) -> P.Writer w a)+  runWriter :: repr h (P.Writer w a -> (a, w))+  swap :: repr h ((l, r) -> (r, l))+  swap = lam $ \p -> mkProd2 (fst1 p) (zro1 p)+  curry :: repr h (((a, b) -> c) -> (a -> b -> c))+  uncurry :: repr h ((a -> b -> c) -> ((a, b) -> c))+  curry = lam3 $ \f a b -> app f (mkProd2 a b)+  uncurry = lam2 $ \f p -> app2 f (zro1 p) (fst1 p)+  float2Double :: repr h (P.Float -> P.Double)+  double2Float :: repr h (P.Double -> P.Float)++class Reify repr x where+  reify :: x -> repr h x++instance Lang repr => Reify repr () where+  reify _ = unit++instance Lang repr => Reify repr P.Double where+  reify = double++instance (Lang repr, Reify repr l, Reify repr r) => Reify repr (l, r) where+  reify (l, r) = mkProd2 (reify l) (reify r)++instance Lang Eval where+  zro = comb P.fst+  fst = comb P.snd+  mkProd = comb (,)+  double = comb+  doublePlus = comb (+)+  doubleMinus = comb (-)+  doubleMult = comb (*)+  doubleDivide = comb (/)+  fix = comb loop+    where loop x = x $ loop x+  left = comb P.Left+  right = comb P.Right+  sumMatch = comb $ \l r -> \case+                             P.Left x -> l x+                             P.Right x -> r x+  unit = comb ()+  exfalso = comb absurd+  nothing = comb P.Nothing+  just = comb P.Just+  ioRet = comb P.return+  ioBind = comb (>>=)+  nil = comb []+  cons = comb (:)+  listMatch = comb $ \l r -> \case+                            [] -> l+                            x:xs -> r x xs+  optionMatch = comb $ \l r -> \case+                              P.Nothing -> l+                              P.Just x -> r x+  ioMap = comb P.fmap+  writer = comb (P.WriterT . P.Identity)+  runWriter = comb P.runWriter+  doubleExp = comb P.exp+  float = comb+  floatPlus = comb (+)+  floatMinus = comb (-)+  floatMult = comb (*)+  floatDivide = comb (/)+  floatExp = comb P.exp+  float2Double = comb P.float2Double+  double2Float = comb P.double2Float++instance Lang Show where+  mkProd = name "mkProd"+  zro = name "zro"+  fst = name "fst"+  double = name . show+  doublePlus = name "plus"+  doubleMinus = name "minus"+  doubleMult = name "mult"+  doubleDivide = name "divide"+  doubleExp = name "exp"+  fix = name "fix"+  left = name "left"+  right = name "right"+  sumMatch = name "sumMatch"+  unit = name "unit"+  exfalso = name "exfalso"+  nothing = name "nothing"+  just = name "just"+  ioRet = name "ioRet"+  ioBind = name "ioBind"+  nil = name "nil"+  cons = name "cons"+  listMatch = name "listMatch"+  optionMatch = name "optionMatch"+  ioMap = name "ioMap"+  writer = name "writer"+  runWriter = name "runWriter"+  float = name . show+  floatPlus = name "plus"+  floatMinus = name "minus"+  floatMult = name "mult"+  floatDivide = name "divide"+  floatExp = name "exp"+  float2Double = name "float2Double"+  double2Float = name "double2Float"++instance Lang repr => Lang (GWDiff repr) where+  mkProd = GWDiff (P.const mkProd)+  zro = GWDiff $ P.const $ zro+  fst = GWDiff $ P.const $ fst+  double x = GWDiff $ P.const $ mkProd2 (double x) zero+  doublePlus = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))+  doubleMinus = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))+  doubleMult = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (mult2 (zro1 l) (zro1 r))+      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))+  doubleDivide = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (divide2 (zro1 l) (zro1 r))+      (divide2 (minus2 (mult2 (zro1 r) (fst1 l)) (mult2 (zro1 l) (fst1 r)))+        (mult2 (zro1 r) (zro1 r)))+  doubleExp = GWDiff $ P.const $ lam $ \x -> mkProd2 (doubleExp1 (zro1 x)) (mult2 (doubleExp1 (zro1 x)) (fst1 x))+  fix = GWDiff $ P.const fix+  left = GWDiff $ P.const left+  right = GWDiff $ P.const right+  sumMatch = GWDiff $ P.const sumMatch+  unit = GWDiff $ P.const unit+  exfalso = GWDiff $ P.const exfalso+  nothing = GWDiff $ P.const nothing+  just = GWDiff $ P.const just+  ioRet = GWDiff $ P.const ioRet+  ioBind = GWDiff $ P.const ioBind+  nil = GWDiff $ P.const nil+  cons = GWDiff $ P.const cons+  listMatch = GWDiff $ P.const listMatch+  optionMatch = GWDiff $ P.const optionMatch+  ioMap = GWDiff $ P.const ioMap+  writer = GWDiff $ P.const writer+  runWriter = GWDiff $ P.const runWriter+  float x = GWDiff $ P.const $ mkProd2 (float x) zero+  floatPlus = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))+  floatMinus = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))+  floatMult = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (mult2 (float2Double1 (zro1 l)) (zro1 r))+      (plus2 (mult2 (float2Double1 (zro1 l)) (fst1 r)) (mult2 (float2Double1 (zro1 r)) (fst1 l)))+  floatDivide = GWDiff $ P.const $ lam2 $ \l r ->+    mkProd2 (divide2 (zro1 l) (float2Double1 (zro1 r)))+      (divide2 (minus2 (mult2 (float2Double1 (zro1 r)) (fst1 l)) (mult2 (float2Double1 (zro1 l)) (fst1 r)))+        (float2Double1 (mult2 (float2Double1 (zro1 r)) (zro1 r))))+  floatExp = GWDiff $ P.const $ lam $ \x -> mkProd2 (floatExp1 (zro1 x)) (mult2 (float2Double1 (floatExp1 (zro1 x))) (fst1 x))+  float2Double = GWDiff $ P.const $ bimap2 float2Double id+  double2Float = GWDiff $ P.const $ bimap2 double2Float id++instance (Vector repr v, Lang repr) => Lang (WDiff repr v) where+  mkProd = WDiff mkProd+  zro = WDiff zro+  fst = WDiff fst+  double x = WDiff $ mkProd2 (double x) zero+  doublePlus = WDiff $ lam2 $ \l r ->+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))+  doubleMinus = WDiff $ lam2 $ \l r ->+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))+  doubleMult = WDiff $ lam2 $ \l r ->+    mkProd2 (mult2 (zro1 l) (zro1 r))+      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))+  doubleDivide = WDiff $ lam2 $ \l r ->+    mkProd2 (divide2 (zro1 l) (zro1 r))+      (divide2 (minus2 (mult2 (zro1 r) (fst1 l)) (mult2 (zro1 l) (fst1 r)))+        (mult2 (zro1 r) (zro1 r)))+  doubleExp = WDiff $ lam $ \x -> mkProd2 (doubleExp1 (zro1 x)) (mult2 (doubleExp1 (zro1 x)) (fst1 x))+  fix = WDiff fix+  left = WDiff left+  right = WDiff right+  sumMatch = WDiff sumMatch+  unit = WDiff unit+  exfalso = WDiff exfalso+  nothing = WDiff nothing+  just = WDiff just+  ioRet = WDiff ioRet+  ioBind = WDiff ioBind+  nil = WDiff nil+  cons = WDiff cons+  listMatch = WDiff listMatch+  optionMatch = WDiff optionMatch+  ioMap = WDiff ioMap+  writer = WDiff writer+  runWriter = WDiff runWriter+  float x = WDiff $ mkProd2 (float x) zero+  floatPlus = WDiff $ lam2 $ \l r ->+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))+  floatMinus = WDiff $ lam2 $ \l r ->+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))+  floatMult = WDiff $ lam2 $ \l r ->+    mkProd2 (mult2 (float2Double1 (zro1 l)) (zro1 r))+      (plus2 (mult2 (float2Double1 (zro1 l)) (fst1 r)) (mult2 (float2Double1 (zro1 r)) (fst1 l)))+  floatDivide = WDiff $ lam2 $ \l r ->+    mkProd2 (divide2 (zro1 l) (float2Double1 (zro1 r)))+      (divide2 (minus2 (mult2 (float2Double1 (zro1 r)) (fst1 l)) (mult2 (float2Double1 (zro1 l)) (fst1 r)))+        (float2Double1 (mult2 (float2Double1 (zro1 r)) (zro1 r))))+  floatExp = WDiff $ lam $ \x -> mkProd2 (floatExp1 (zro1 x)) (mult2 (float2Double1 (floatExp1 (zro1 x))) (fst1 x))+  float2Double = WDiff $ bimap2 float2Double id+  double2Float = WDiff $ bimap2 double2Float id++instance Lang repr => ProdCon (Monoid repr) l r where prodCon = Sub Dict++instance Lang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict++instance Lang repr => ProdCon (Reify repr) l r where prodCon = Sub Dict++instance Lang repr => ProdCon (Vector repr) l r where prodCon = Sub Dict++instance Lang repr => Lang (ImpW repr) where+  nil = NoImpW nil+  cons = NoImpW cons+  listMatch = NoImpW listMatch+  zro = NoImpW zro+  fst = NoImpW fst+  mkProd = NoImpW mkProd+  ioRet = NoImpW ioRet+  ioMap = NoImpW ioMap+  ioBind = NoImpW ioBind+  unit = NoImpW unit+  nothing = NoImpW nothing+  just = NoImpW just+  optionMatch = NoImpW optionMatch+  exfalso = NoImpW exfalso+  fix = NoImpW fix+  left = NoImpW left+  right = NoImpW right+  sumMatch = NoImpW sumMatch+  writer = NoImpW writer+  runWriter = NoImpW runWriter+  double = NoImpW . double+  doubleExp = NoImpW doubleExp+  doublePlus = NoImpW doublePlus+  doubleMinus = NoImpW doubleMinus+  doubleMult = NoImpW doubleMult+  doubleDivide = NoImpW doubleDivide+  float = NoImpW . float+  floatExp = NoImpW floatExp+  floatPlus = NoImpW floatPlus+  floatMinus = NoImpW floatMinus+  floatMult = NoImpW floatMult+  floatDivide = NoImpW floatDivide+  float2Double = NoImpW float2Double+  double2Float = NoImpW double2Float++instance (Lang l, Lang r) => Lang (Combine l r) where+  mkProd = Combine mkProd mkProd+  zro = Combine zro zro+  fst = Combine fst fst+  double x = Combine (double x) (double x)+  doublePlus = Combine doublePlus doublePlus+  doubleMinus = Combine doubleMinus doubleMinus+  doubleMult = Combine doubleMult doubleMult+  doubleDivide = Combine doubleDivide doubleDivide+  doubleExp = Combine doubleExp doubleExp+  float x = Combine (float x) (float x)+  floatPlus = Combine floatPlus floatPlus+  floatMinus = Combine floatMinus floatMinus+  floatMult = Combine floatMult floatMult+  floatDivide = Combine floatDivide floatDivide+  floatExp = Combine floatExp floatExp+  fix = Combine fix fix+  left = Combine left left+  right = Combine right right+  sumMatch = Combine sumMatch sumMatch+  unit = Combine unit unit+  exfalso = Combine exfalso exfalso+  nothing = Combine nothing nothing+  just = Combine just just+  optionMatch = Combine optionMatch optionMatch+  ioRet = Combine ioRet ioRet+  ioBind = Combine ioBind ioBind+  ioMap = Combine ioMap ioMap+  nil = Combine nil nil+  cons = Combine cons cons+  listMatch = Combine listMatch listMatch+  runWriter = Combine runWriter runWriter+  writer = Combine writer writer+  double2Float = Combine double2Float double2Float+  float2Double = Combine float2Double float2Double++instance Lang repr => WithDiff repr () where+  withDiff = const1 id++instance Lang repr => WithDiff repr P.Double where+  withDiff = lam2 $ \conv d -> mkProd2 d (app conv doubleOne)++instance (Lang repr, WithDiff repr l, WithDiff repr r) => WithDiff repr (l, r) where+  withDiff = lam $ \conv -> bimap2 (withDiff1 (lam $ \l -> app conv (mkProd2 l zero))) (withDiff1 (lam $ \r -> app conv (mkProd2 zero r)))++class Monoid r g => Group r g where+  invert :: r h (g -> g)+  minus :: r h (g -> g -> g)+  default invert :: Lang r => r h (g -> g)+  invert = minus1 zero+  default minus :: Lang r => r h (g -> g -> g)+  minus = lam2 $ \x y -> plus2 x (invert1 y)+  {-# MINIMAL (invert | minus) #-}++class Group r v => Vector r v where+  mult :: r h (P.Double -> v -> v)+  divide :: r h (v -> P.Double -> v)+  default mult :: Lang r => r h (P.Double -> v -> v)+  mult = lam2 $ \x y -> divide2 y (recip1 x)+  default divide :: Lang r => r h (v -> P.Double -> v)+  divide = lam2 $ \x y -> mult2 (recip1 y) x+  {-# MINIMAL (mult | divide) #-}++instance Lang r => Monoid r () where+  zero = unit+  plus = const1 $ const1 unit++instance Lang r => Group r () where+  invert = const1 unit+  minus = const1 $ const1 unit++instance Lang r => Vector r () where+  mult = const1 $ const1 unit+  divide = const1 $ const1 unit++instance Lang r => Monoid r P.Double where+  zero = doubleZero+  plus = doublePlus++instance Lang r => Group r P.Double where+  minus = doubleMinus++instance Lang r => Vector r P.Double where+  mult = doubleMult+  divide = doubleDivide++instance Lang r => Monoid r P.Float where+  zero = floatZero+  plus = floatPlus++instance Lang r => Group r P.Float where+  minus = floatMinus++instance Lang r => Vector r P.Float where+  mult = com2 floatMult double2Float+  divide = com2 (flip2 com double2Float) floatDivide++instance (Lang repr, Monoid repr l, Monoid repr r) => Monoid repr (l, r) where+  zero = mkProd2 zero zero+  plus = lam2 $ \l r -> mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))++instance (Lang repr, Group repr l, Group repr r) => Group repr (l, r) where+  invert = bimap2 invert invert++instance (Lang repr, Vector repr l, Vector repr r) => Vector repr (l, r) where+  mult = lam $ \x -> bimap2 (mult1 x) (mult1 x)++instance (Lang repr, Monoid repr l, Monoid repr r) => Monoid repr (l -> r) where+  zero = const1 zero+  plus = lam3 $ \l r x -> plus2 (app l x) (app r x)++instance (Lang repr, Group repr l, Group repr r) => Group repr (l -> r) where+  invert = lam2 $ \l x -> app l (invert1 x)++instance (Lang repr, Vector repr l, Vector repr r) => Vector repr (l -> r) where+  mult = lam3 $ \l r x -> app r (mult2 l x)++instance Lang r => Monoid r [a] where+  zero = nil+  plus = listAppend++instance Lang r => Functor r [] where+  map = lam $ \f -> fix1 $ lam $ \self -> listMatch2 nil (lam2 $ \x xs -> cons2 (app f x) $ app self xs)++instance Lang r => BiFunctor r (,) where+  bimap = lam3 $ \l r p -> mkProd2 (app l (zro1 p)) (app r (fst1 p))++instance Lang r => Functor r (P.Writer w) where+  map = lam $ \f -> com2 writer (com2 (bimap2 f id) runWriter)++instance (Lang r, Monoid r w) => Applicative r (P.Writer w) where+  pure = com2 writer (flip2 mkProd zero)+  ap = lam2 $ \f x -> writer1 (mkProd2 (app (zro1 (runWriter1 f)) (zro1 (runWriter1 x))) (plus2 (fst1 (runWriter1 f)) (fst1 (runWriter1 x))))++instance (Lang r, Monoid r w) => Monad r (P.Writer w) where+  join = lam $ \x -> writer1 $ mkProd2 (zro1 $ runWriter1 $ zro1 $ runWriter1 x) (plus2 (fst1 $ runWriter1 $ zro1 $ runWriter1 x) (fst1 $ runWriter1 x))++instance Lang r => Functor r P.IO where+  map = ioMap++instance Lang r => Applicative r P.IO where+  pure = ioRet+  ap = lam2 $ \f x -> ioBind2 f (flip2 ioMap x)++instance Lang r => Monad r P.IO where+  bind = ioBind++instance Lang r => Functor r P.Maybe where+  map = lam $ \func -> optionMatch2 nothing (com2 just func)++instance Lang r => Applicative r P.Maybe where+  pure = just+  ap = optionMatch2 (const1 nothing) map++instance Lang r => Monad r P.Maybe where+  bind = lam2 $ \x func -> optionMatch3 nothing func x++runImpW :: forall repr h x. Lang repr => ImpW repr h x -> RunImpW repr h x+runImpW (ImpW x) = RunImpW x+runImpW (NoImpW x) = RunImpW (const1 x :: repr h (() -> x))++newtype GWDiff repr h x = GWDiff {runGWDiff :: forall v. Vector repr v => Proxy v -> repr (Diff v h) (Diff v x)}++instance DBI repr => DBI (GWDiff repr) where+  z = GWDiff (P.const z)+  s (GWDiff x) = GWDiff (\p -> s $ x p)+  app (GWDiff f) (GWDiff x) = GWDiff (\p -> app (f p) (x p))+  abs (GWDiff x) = GWDiff (\p -> abs $ x p)++cons2 = app2 cons+listMatch2 = app2 listMatch+fix1 = app fix+fix2 = app2 fix+uncurry1 = app uncurry+optionMatch2 = app2 optionMatch+optionMatch3 = app3 optionMatch+zro1 = app zro+fst1 = app fst+mult1 = app mult+mult2 = app2 mult+divide2 = app2 divide+invert1 = app invert+mkProd1 = app mkProd+mkProd2 = app2 mkProd+minus1 = app minus+divide1 = app divide+recip = divide1 doubleOne+recip1 = app recip+writer1 = app writer+runWriter1 = app runWriter+ioBind2 = app2 ioBind+minus2 = app2 minus+float2Double1 = app float2Double+doubleExp1 = app doubleExp+floatExp1 = app floatExp++instance Lang repr => DBI (ImpW repr) where+  z = NoImpW z+  s :: forall a h b. ImpW repr h b -> ImpW repr (a, h) b+  s (ImpW x) = work x+    where+      work :: Weight w => repr h (w -> b) -> ImpW repr (a, h) b+      work x = ImpW (s x)+  s (NoImpW x) = NoImpW (s x)+  app (ImpW f) (ImpW x) = ImpW (lam $ \p -> app (app (conv f) (zro1 p)) (app (conv x) (fst1 p)))+  app (NoImpW f) (NoImpW x) = NoImpW (app f x)+  app (ImpW f) (NoImpW x) = ImpW (lam $ \w -> app2 (conv f) w (conv x))+  app (NoImpW f) (ImpW x) = ImpW (lam $ \w -> app (conv f) (app (conv x) w))+  abs (ImpW f) = ImpW (flip1 $ abs f)+  abs (NoImpW x) = NoImpW (abs x)

@@ -1,19 +0,0 @@-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    NoMonomorphismRestriction #-}
-
-module Main (main) where
-import qualified HOAS
-import qualified Comb
-import qualified DBI
-import qualified Poly
-
-main = Poly.main

@@ -16,18 +16,19 @@ > module Poly where
 > import Control.Monad (when)
 > import Util
-> import DBI hiding (main, return)
+> import DBI hiding (return)
+> import Lang
 
 Importing files and opening language extension...
 So, our goal is to find x, where x * x + 2 * x + 3 = 27.
 To do so, we try to minimize their difference squared (l2 norm).
 
-> poly :: forall repr h. DBI repr => repr h (Double -> Double)
-> poly = hlam $ \x -> plus2 (mult2 x x) (plus2 (mult2 (lit 2.0) x) (lit 3.0))
+> poly :: forall repr h. Lang repr => repr h (Double -> Double)
+> poly = lam $ \x -> plus2 (mult2 x x) (plus2 (mult2 (double 2.0) x) (double 3.0))
 
 poly x = x * x + (2 * x + 3)
 
-> l2 = hlam $ \x -> mult2 (minus2 x (lit 27)) (minus2 x (lit 27))
+> l2 = lam $ \x -> mult2 (minus2 x (double 27)) (minus2 x (double 27))
 
 l2 x = (x - 27) * (x - 27)
 l2 measure how far is the input from 27

@@ -1,22 +1,4 @@-> {-# LANGUAGE->     MultiParamTypeClasses,->     RankNTypes,->     ScopedTypeVariables,->     FlexibleInstances,->     FlexibleContexts,->     UndecidableInstances,->     PolyKinds,->     LambdaCase,->     NoMonomorphismRestriction,->     TypeFamilies,->     LiberalTypeSynonyms,->     EmptyCase,->     FunctionalDependencies,->     ExistentialQuantification,->     InstanceSigs,->     TupleSections,->     ConstraintKinds,->     AllowAmbiguousTypes #-}+> {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications #-}  This is the classical example of using sigmoid NN to approximate Xor. @@ -28,6 +10,9 @@ > import Util > import System.Random > import Control.Monad (when)+> import Data.Proxy+> import Data.Constraint+> import Lang  Recall in poly, we constructed a function Double -> Double, with argument being the weight, and do gradient descend to found a solution.@@ -45,7 +30,7 @@  Let's start by constructing a weight. -> weight :: DBI repr => ImpW repr h Double+> weight :: Lang repr => ImpW repr h Double > weight = ImpW id  Note that we are just manipulating AST.@@ -55,72 +40,72 @@  We have the weight, now we need the activation function, sigmoid. -> sigmoid = hlam $ \x -> recip1 (plus2 litOne (exp1 (invert1 x)))+> sigmoid = lam $ \x -> recip1 (plus2 doubleOne (doubleExp1 (invert1 x))) > sigmoid1 = app sigmoid  With weight and sigmoid we can construct a neuron of type ((Double, Double) -> Double) The weight should be a pair of Double, each as a scale on the actual input, with a bias. We then add the two scaled input, with the bias, and pass them into sigmoid. -> scaleAdd :: DBI repr => ImpW repr h ((Double, Double) -> Double)-> scaleAdd = ImpW $ hlam2 $ \w p -> plus2 (mult2 (zro1 w) (zro1 p)) (plus2 (fst1 w) (fst1 p))+> scaleAdd :: Lang repr => ImpW repr h ((Double, Double) -> Double)+> scaleAdd = ImpW $ lam2 $ \w p -> plus2 (mult2 (zro1 w) (zro1 p)) (plus2 (fst1 w) (fst1 p)) -> withBias :: DBI repr => ImpW repr h (Double -> Double)+> withBias :: Lang repr => ImpW repr h (Double -> Double) > withBias = ImpW $ plus -> neuron :: DBI repr => ImpW repr h ((Double, Double) -> Double)+> neuron :: Lang repr => ImpW repr h ((Double, Double) -> Double) > neuron = com2 (com2 sigmoid withBias) scaleAdd > neuron1 = app neuron  Now, the hidden layer of type (Double, Double) -> ((Double, Double), (Double, Double)) -> hidden = hlam $ \p -> mkProd2 (mkProd2 (neuron1 p) (neuron1 p)) (mkProd2 (neuron1 p) (neuron1 p))+> hidden = lam $ \p -> mkProd2 (mkProd2 (neuron1 p) (neuron1 p)) (mkProd2 (neuron1 p) (neuron1 p))  And finally, the whole NN:  > type XOR = (Double, Double) -> Double-> xor :: DBI repr => ImpW repr h XOR+> xor :: Lang repr => ImpW repr h XOR > xor = neuron `com2` (bimap2 scaleAdd scaleAdd) `com2` hidden  But before we can train it, we need to define the dataset and the loss function. -> l2 :: DBI repr => repr h (Double -> Double -> Double)-> l2 = hlam2 $ \l r -> (mult2 (minus2 l r) (minus2 l r))+> l2 :: Lang repr => repr h (Double -> Double -> Double)+> l2 = lam2 $ \l r -> (mult2 (minus2 l r) (minus2 l r)) > l22 = app2 l2 -> eval :: DBI repr => repr h (XOR -> ((Double, Double), Double) -> Double)-> eval = hlam2 $ \xor p -> l22 (app xor (zro1 p)) (fst1 p)+> eval :: Lang repr => repr h (XOR -> ((Double, Double), Double) -> Double)+> eval = lam2 $ \xor p -> l22 (app xor (zro1 p)) (fst1 p) -> dataset :: DBI repr => repr h [((Double, Double), Double)]+> dataset :: Lang repr => repr h [((Double, Double), Double)] > dataset = cons2 (build 0 0 0) (cons2 (build 0 1 1) (cons2 (build 1 0 1) (cons2 (build 1 1 0) nil)))->   where build l r ret = mkProd2 (mkProd2 (lit l) (lit r)) (lit ret)+>   where build l r ret = mkProd2 (mkProd2 (double l) (double r)) (double ret)  However, unlike Poly, there are more than one datapoint, so we need to use a list, and map xor onto it. -> loss :: DBI repr => repr h (XOR -> Double)-> loss = hlam $ \xor -> fix2 (hlam $ \self -> listMatch2 litZero (hlam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)+> loss :: Lang repr => repr h (XOR -> Double)+> loss = lam $ \xor -> fix2 (lam $ \self -> listMatch2 doubleZero (lam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)  Let's try to print the thing.  > main :: IO () > main = case runImpW $ noEnv xor of RunImpW xor -> inner xor >   where->     inner :: forall w. Weight (Term DBI) w => Term DBI () (w -> (Double, Double) -> Double) -> IO ()->     inner (Term xor) = do->       print $ runShow xor vars 0+>     inner :: forall w. Weight w => Combine Show (GWDiff Eval) () (w -> (Double, Double) -> Double) -> IO ()+>     inner (Combine xorS xorE) = do+>       print $ runShow xorS vars 0  now you will see a list of gibberish ->       initWeight :: w <- randomRIO (randRange (-0.01, 0.01))+>       initWeight :: w <- ((randomRIO (randRange (-0.01, 0.01)) \\ weightCon @w @Random) \\ weightCon @w @RandRange)  Getting random weights... ->       diffAST (runWDiff xor :: Term DBI () (Diff w (w -> XOR))) initWeight->         (selfWithDiff :: Term DBI () (w -> Diff w w)) (runWDiff $ noEnv loss :: Term DBI () (Diff w (XOR -> Double)))->         ((hlam3 $ \d o n -> minus2 o (mult2 d n)) :: Term DBI () (Double -> w -> w -> w))->     diffAST (Term xor) weight (Term wdiff) (Term loss) (Term update) =->       go (runEval xor ()) weight (runEval wdiff ()) (runEval loss ()) (runEval update ()) 0->     go :: forall w. P.Show w => (Diff w (w -> XOR)) -> w -> (w -> Diff w w) -> (Diff w (XOR -> Double)) -> (Double -> w -> w -> w) -> Int -> IO ()+>       (go (diff xorE) initWeight (runEval selfWithDiff () \\ weightCon @w @(WithDiff Eval)) (diff loss)+>           ((runEval (lam3 $ \d o n -> minus2 o (mult2 d n)) ()) \\ weightCon @w @(Vector Eval)) 0) \\ weightCon @w @P.Show+>         where+>           diff :: GWDiff Eval () x -> Diff w x+>           diff x = (runEval (runGWDiff x (Proxy :: Proxy w)) ()) \\ weightCon @w @(Vector Eval)+>     go :: P.Show w => (Diff w (w -> XOR)) -> w -> (w -> Diff w w) -> (Diff w (XOR -> Double)) -> (Double -> w -> w -> w) -> Int -> IO () >     go xor weight reify loss update i | i <= 2500 = do >       when (isSquare i) $ do >         print weight