Core Simplicity Terms and Types for both Coq and Haskell libraries.

Basic bit and arithmetic Simplicity expressions for Haskell.
Outline and description of Core Simplicity for the Tech Report.

Coq/Simplicity/Core.v

@@ -0,0 +1,30 @@
+Require Import Ty.
+
+Inductive Term : Ty -> Ty -> Set :=
+| iden : forall {A : Ty}, Term A A
+| comp : forall {A B C : Ty}, Term A B -> Term B C -> Term A C
+| unit : forall {A : Ty}, Term A Unit
+| injl : forall {A B C : Ty}, Term A B -> Term A (Sum B C)
+| injr : forall {A B C : Ty}, Term A C -> Term A (Sum B C)
+| case : forall {A B C D : Ty},
+    Term (Prod A C) D -> Term (Prod B C) D -> Term (Prod (Sum A B) C) D
+| pair : forall {A B C : Ty}, Term A B -> Term A C -> Term A (Prod B C)
+| take : forall {A B C : Ty}, Term A C -> Term (Prod A B) C
+| drop : forall {A B C : Ty}, Term B C -> Term (Prod A B) C.
+
+Fixpoint eval {A B : Ty} (x : Term A B) : tySem A -> tySem B :=
+match x in Term A B return tySem A -> tySem B with
+| iden => fun a => a
+| comp s t => fun a => eval t (eval s a)
+| unit => fun _ => tt
+| injl t => fun a => inl (eval t a)
+| injr t => fun a => inr (eval t a)
+| case s t => fun p => let (ab, c) := p in
+    match ab with
+    | inl a => eval s (a, c)
+    | inr b => eval t (b, c)
+    end
+| pair s t => fun a => (eval s a, eval t a)
+| take t => fun ab => eval t (fst ab)
+| drop t => fun ab => eval t (snd ab)
+end.

Coq/Simplicity/Ty.v

@@ -0,0 +1,11 @@
+Inductive Ty : Set :=
+| Unit : Ty
+| Sum  : Ty -> Ty -> Ty
+| Prod : Ty -> Ty -> Ty.
+
+Fixpoint tySem (X : Ty) : Set :=
+match X with
+| Unit => Datatypes.unit
+| Sum A B => tySem A + tySem B
+| Prod A B => tySem A * tySem B
+end.

Haskell/Simplicity/Arith.hs

@@ -0,0 +1,69 @@
+{-# LANGUAGE GADTs #-}
+module Simplicity.Arith
+  ( Word(..), wordTy
+  , adder, fullAdder
+  , multiplier, fullMultiplier
+  ) where
+
+import Simplicity.Bit
+import Simplicity.Ty
+import Simplicity.Term
+
+import Prelude hiding (Word, drop, take, not, or)
+
+data Word a where
+  BitW :: Word Bit
+  DoubleW :: Word a -> Word (a,a)
+
+wordTy :: Word a -> TyReflect a
+wordTy BitW = SumR OneR OneR
+wordTy (DoubleW w) = ProdR rec rec
+ where
+  rec = wordTy w
+
+adder :: Core term => Word a -> term (a, a) (Bit, a)
+adder BitW = cond (iden &&& not iden) (false &&& iden)
+adder (DoubleW w) = (take (take iden) &&& drop (take iden))
+                &&& (take (drop iden) &&& drop (drop iden) >>> rec)
+                >>> (take iden &&& drop (take iden) >>> fa) &&& drop (drop iden)
+                >>> take (take iden) &&& (take (drop iden) &&& drop iden)
+ where
+  rec = adder w
+  fa = fullAdder w
+
+fullAdder :: Core term => Word a -> term ((a, a), Bit) (Bit, a)
+fullAdder BitW = take add &&& drop iden
+             >>> take (take iden) &&& (take (drop iden) &&& drop iden >>> add)
+             >>> cond true (take iden) &&& drop (drop iden)
+ where
+  add = adder BitW
+fullAdder (DoubleW w) = take (take (take iden) &&& drop (take iden))
+                    &&& (take (take (drop iden) &&& drop (drop iden)) &&& drop iden >>> rec)
+                    >>> (take iden &&& drop (take iden) >>> rec) &&& drop (drop iden)
+                    >>> take (take iden) &&& (take (drop iden) &&& drop iden)
+ where
+  rec = fullAdder w
+
+fullMultiplier :: Core term => Word a -> term ((a, a), (a, a)) (a, a)
+fullMultiplier BitW = drop iden &&& take (cond iden false)
+                  >>> fullAdder BitW
+fullMultiplier (DoubleW w) = take ((take (take iden) &&& drop (take iden)) &&& take (drop iden))
+                         &&& ((take (take (take iden) &&& drop (drop iden)) &&& drop (take (take iden) &&& drop (take iden)) >>> rec)
+                         &&& (take (take (drop iden) &&& drop (drop iden)) &&& drop (take (drop iden) &&& drop (drop iden)) >>> rec))
+                         >>> (take (take iden) &&& (take (take (drop iden) &&& drop iden) &&& drop (take (drop iden) &&& drop (take iden)) >>> rec))
+                         &&& (drop (take (take iden) &&& drop (drop iden)))
+                         >>> (take (take iden) &&& (take (drop (take iden)) &&& drop (take iden)) >>> rec) &&& (take (drop (drop iden)) &&& drop (drop iden))
+ where
+  rec = fullMultiplier w
+
+multiplier :: Core term => Word a -> term (a, a) (a, a)
+multiplier BitW = false &&& cond iden false
+multiplier (DoubleW w) = ((take (take iden) &&& drop (take iden)) &&& take (drop iden))
+                     &&& ((take (take iden) &&& drop (drop iden) >>> rec)
+                     &&& (take (drop iden) &&& drop (drop iden) >>> rec))
+                     >>> (take (take iden) &&& (take (take (drop iden) &&& drop iden) &&& drop (take (drop iden) &&& drop (take iden)) >>> fmul))
+                     &&& (drop (take (take iden) &&& drop (drop iden)))
+                     >>> (take (take iden) &&& (take (drop (take iden)) &&& drop (take iden)) >>> fmul) &&& (take (drop (drop iden)) &&& drop (drop iden))
+ where
+  rec = multiplier w
+  fmul = fullMultiplier w

Haskell/Simplicity/Bit.hs

@@ -0,0 +1,27 @@
+module Simplicity.Bit 
+ ( Bit, false, true, cond, not, and, or
+ ) where
+
+import Prelude hiding (drop, take, not, and, or)
+
+import Simplicity.Term
+
+type Bit = Either () ()
+
+false :: Core term => term a Bit
+false = injl unit
+
+true :: Core term => term a Bit
+true = injr unit
+
+cond :: Core term => term a b -> term a b -> term (Bit, a) b
+cond thn els = match (drop els) (drop thn)
+
+not :: Core term => term a Bit -> term a Bit
+not t = pair t unit >>> cond false true
+
+and :: Core term => term a Bit -> term a Bit -> term a Bit
+and s t = pair s iden >>> cond t false
+
+or :: Core term => term a Bit -> term a Bit -> term a Bit
+or s t = pair s iden >>> cond true t

Haskell/Simplicity/Generic.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+module Simplicity.Generic
+  ( scribe
+  , eq
+  ) where
+
+import Prelude hiding (drop, take)
+
+import Simplicity.Bit
+import Simplicity.Term
+import Simplicity.Ty
+
+scribe :: Core term => TyReflect b -> b -> term a b
+scribe OneR          ()        = unit
+scribe (SumR l _)    (Left v)  = injl (scribe l v)
+scribe (SumR _ r)    (Right v) = injr (scribe r v)
+scribe (ProdR b1 b2) (v1, v2)  = pair (scribe b1 v1) (scribe b2 v2)
+
+eq :: Core term => TyReflect a -> term (a, a) Bit
+eq OneR          = true
+eq (SumR l r)    = match (pair (drop iden) (take iden) >>> match (eq l) false)
+                         (pair (drop iden) (take iden) >>> match false (eq r))
+eq (ProdR a1 a2) = pair (pair (take (take iden)) (drop (take iden)) >>> (eq a1))
+                        (pair (take (drop iden)) (drop (drop iden)))
+                   >>> cond (eq a2) false

Haskell/Simplicity/Term.hs

@@ -0,0 +1,39 @@
+module Simplicity.Term
+ ( Category, iden, comp, (>>>), (&&&)
+ , Core, unit, injl, injr, match, pair, take, drop
+ ) where
+
+import Control.Category (Category, (>>>))
+import qualified Control.Category as Cat
+import Prelude hiding (take, drop)
+
+-- same precidence as in Control.Arrow.
+infixr 3 &&&
+
+iden :: Category term => term a a
+iden = Cat.id
+
+comp :: Category term => term a b -> term b c -> term a c
+comp = (>>>)
+
+class Category term => Core term where
+  unit :: term a ()
+  injl :: term a b -> term a (Either b c)
+  injr :: term a c -> term a (Either b c)
+  match :: term (a, c) d -> term (b, c) d -> term (Either a b, c) d
+  pair :: term a b -> term a c -> term a (b, c)
+  take :: term a c -> term (a, b) c
+  drop :: term b c -> term (a, b) c
+
+(&&&) :: Core term => term a b -> term a c -> term a (b, c)
+(&&&) = pair
+
+instance Core (->) where
+  unit = const ()
+  injl t a = Left (t a)
+  injr t a = Right (t a)
+  match s _ (Left a, c)  = s (a, c)
+  match _ t (Right b, c) = t (b, c)
+  pair s t a = (s a, t a)
+  take t (a, _) = t a
+  drop t (_, b) = t b

Haskell/Simplicity/Ty.hs

@@ -0,0 +1,51 @@
+{-# LANGUAGE GADTs, TypeOperators, DeriveTraversable #-}
+module Simplicity.Ty
+ ( TyF(..), Ty
+ , one, sum, prod
+ , TyReflect(..)
+ , equalTyReflect
+ ) where
+
+import Control.Unification.Types (Unifiable, zipMatch)
+import Data.Functor.Fixedpoint (Fix(..))
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding (sum, prod)
+
+data TyF a = One
+           | Sum a a
+           | Prod a a 
+           deriving (Eq, Functor, Foldable, Traversable)
+
+type Ty = Fix TyF
+
+one :: Ty
+one = Fix One
+
+sum :: Ty -> Ty -> Ty
+sum a b = Fix $ Sum a b
+
+prod :: Ty -> Ty -> Ty
+prod a b = Fix $ Prod a b
+
+instance Unifiable TyF where
+  zipMatch One One = Just One
+  zipMatch (Sum a1 b1) (Sum a2 b2) = Just (Sum (Right (a1, a2)) (Right (b1, b2)))
+  zipMatch (Prod a1 b1) (Prod a2 b2) = Just (Prod (Right (a1, a2)) (Right (b1, b2)))
+  zipMatch _ _ = Nothing
+
+data TyReflect a where
+  OneR :: TyReflect ()
+  SumR  :: TyReflect a -> TyReflect b -> TyReflect (Either a b)
+  ProdR :: TyReflect a -> TyReflect b -> TyReflect (a, b)
+
+equalTyReflect :: TyReflect a -> TyReflect b -> Maybe (a :~: b)
+equalTyReflect OneR OneR = return Refl
+equalTyReflect (SumR a1 b1) (SumR a2 b2) = do
+  Refl <- equalTyReflect a1 a2
+  Refl <- equalTyReflect b1 b2
+  return Refl
+equalTyReflect (ProdR a1 b1) (ProdR a2 b2) = do
+  Refl <- equalTyReflect a1 a2
+  Refl <- equalTyReflect b1 b2
+  return Refl
+equalTyReflect _ _ = Nothing

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain