From 2f9d8a6ce68249fae08ed3ac63ed18ceb23baebf Mon Sep 17 00:00:00 2001 From: "adam.gundry" Date: Thu, 20 Oct 2011 14:08:35 +0100 Subject: [PATCH] Wires example and a funny thing in induction Ignore-this: ffd5313d5d0c7454b736ac0f12abd813 darcs-hash:20111020130835-e29d1-76a5a64e47a315fdb7fd7fd477b839249e04cd75.gz --- Induction.hs | 11 ++- Wires.hs | 194 +++++++++++++++++++++++++++++++++++++++++++++++++ WiresExtras.hs | 34 +++++++++ 3 files changed, 238 insertions(+), 1 deletion(-) create mode 100644 Wires.hs create mode 100644 WiresExtras.hs diff --git a/Induction.hs b/Induction.hs index 1dee276..092dea2 100644 --- a/Induction.hs +++ b/Induction.hs @@ -53,10 +53,19 @@ indy :: forall (f :: Nat -> Nat)(m :: Nat) b . 0 <= f 0 => ProxyNN f -> (0 <= f m => b) -> b indy _ lie s e = lie (Proxy :: Proxy (f m)) e +{- possy :: forall a (m n :: Nat) . (forall (x :: Num) a . Proxy x -> (0 <= x => a) -> a) -> (0 <= m * n => a) -> a possy lie = let foo :: forall (n :: Nat) a . 0 <= m * n => (0 <= m * (n + 1) => a) -> a foo x = x - in indy (ProxyNN :: ProxyNN ((*) m)) lie foo \ No newline at end of file + in indy (ProxyNN :: ProxyNN ((*) m)) lie foo +-} + + + +foo :: forall (f :: Num -> Num -> Num) a . + (forall (m n :: Num) a . Proxy m -> Proxy n -> (f m n ~ f n m => a) -> a) -> + (f 1 3 ~ f 3 1 => a) -> a +foo comm x = comm (Proxy :: Proxy 1) (Proxy :: Proxy 3) x \ No newline at end of file diff --git a/Wires.hs b/Wires.hs new file mode 100644 index 0000000..bc3cbd1 --- /dev/null +++ b/Wires.hs @@ -0,0 +1,194 @@ +{-# OPTIONS_GHC -F -pgmF ./toy #-} +{-# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables, + NPlusKPatterns #-} + +module Wires where + +data Vec :: Num -> * -> * where + VNil :: forall a . Vec 0 a + VCons :: forall (n :: Num) a . 0 <= n => a -> Vec n a -> Vec (n+1) a + +vhead :: forall a (m :: Num) . 0 < m => Vec m a -> a +vhead (VCons x xs) = x + +rev :: forall a (m :: Nat) . Vec m a -> Vec m a +rev = let revapp :: forall (n k :: Nat) . Vec n a -> Vec k a -> Vec (n+k) a + revapp xs VNil = xs + revapp xs (VCons y ys) = revapp (VCons y xs) ys + in revapp VNil + +data Wire :: Num -> * -> Num -> * -> * where + Stop :: forall a b . Wire 0 a 0 b + Say :: forall (m n :: Nat) a b . + b -> Wire m a n b -> Wire m a (n+1) b + Ask :: forall (m n :: Nat) a b . + (a -> Wire m a n b) -> Wire (m+1) a n b + +run :: forall (m n :: Num) a b . Wire m a n b -> Vec m a -> Vec n b +run Stop VNil = VNil +run (Say a p) xs = VCons a (run p xs) +run (Ask f) (VCons x xs) = run (f x) xs + + +sequ :: forall (m n i j :: Num) a b . 0 <= n, 0 <= j => + Wire m a i b -> Wire n a j b -> Wire (m + n) a (i + j) b +sequ Stop q = q +sequ (Say b p) q = Say b (sequ p q) +sequ (Ask f) q = Ask (\ x -> sequ (f x) q) + + +data Proxy :: Num -> * where + Proxy :: forall (n :: Num) . Proxy n + +nsequ :: forall (m n :: Nat) a b . + (forall (x y :: Nat) t . Proxy x -> Proxy y -> (0 <= x * y => t) -> t) -> + (pi (k :: Nat) . Wire m a n b -> Wire (m * k) a (n * k) b) +nsequ lem {0} p = Stop +nsequ lem {k+1} p = lem (Proxy :: Proxy m) (Proxy :: Proxy k) + (lem (Proxy :: Proxy n) (Proxy :: Proxy k) + (sequ p (nsequ lem {k} p))) + + +pipe :: forall (m n i :: Num) a b c . 0 <= m => + Wire m a n b -> Wire n b i c -> Wire m a i c +pipe Stop Stop = Stop +pipe (Ask f) Stop = Ask (\ x -> pipe (f x) Stop) +pipe p (Say b q) = Say b (pipe p q) +pipe (Say x p) (Ask g) = pipe p (g x) +pipe (Ask f) (Ask g) = Ask (\ x -> pipe (f x) (Ask g)) + +always p = Ask (\ zzz -> p) + +bool t f True = t +bool t f False = f + +askB t f = Ask (bool t f) + +wire = Ask (\ a -> Say a Stop) +notGate = Ask (\ b -> Say (not b) Stop) +andGate = askB wire (always (Say False Stop)) +split = Ask (\ a -> Say a (Say a Stop)) +cross = Ask (\ a -> Ask (\ b -> Say b (Say a Stop))) + +mkGate tt tf ft ff = askB (askB (Say tt Stop) (Say tf Stop)) + (askB (Say ft Stop) (Say ff Stop)) + +orGate = mkGate True True True False +nandGate = pipe andGate notGate +norGate = pipe orGate notGate +xorGate = askB notGate wire + +wires :: forall a. pi (n :: Num) . 0 <= n => Wire n a n a +wires {0} = Stop +wires {n+1} = sequ wire (wires {n}) + +manyWires = wires {1000} +sillyWires {n} = wires {1000000*n} + +bind :: forall (m n j :: Num) a . 0 < n, 0 < j => + Wire m a 1 a -> (a -> Wire n a j a) -> Wire (m + n) a j a +bind (Say a p) g = sequ p (g a) +bind (Ask f) g = Ask (\ x -> bind (f x) g) + + + +v2i :: forall (n :: Num) . Vec n Bool -> Integer +v2i VNil = 0 +v2i (VCons True xs) = 1 + (2 * (v2i xs)) +v2i (VCons False xs) = 2 * (v2i xs) + + +odd' :: pi (n :: Nat) . Bool +odd' {0} = False +odd' {n+1} = not (odd' {n}) + +half :: forall a. pi (n :: Nat) . (pi (m r :: Nat) . n ~ 2 * m + r, r <= 1 => a) -> a +half {0} f = f {0} {0} +half {n+1} f = let + g :: pi (m r :: Nat) . n ~ 2 * m + r, r <= 1 => a + g {m} {0} = f {m} {1} + g {m} {1} = f {m+1} {0} + in half {n} g + +-- This needs 2^(x + y) ~> 2^x * 2^y + +toBin' :: pi (m n :: Nat) . n < 2^m => Vec m Bool +toBin' {0} {n} = VNil +toBin' {m+1} {n} = half {n} (\ {k} {r} -> VCons (odd' {r}) (toBin' {m} {k})) + +toBin :: pi (m n :: Nat) . n < 2^m => Vec m Bool +toBin {m} {n} = rev (toBin' {m} {n}) + +-- A real implementation of div/mod might be nice + +divvy :: forall a. pi (n d :: Nat) . d >= 1 => (pi (m r :: Nat) . n ~ d * m + r, r < d => a) -> a +divvy {n} {d} f | {n < d} = f {0} {n} +divvy {n} {d} f | {n >= d} = + let g :: pi (m r :: Nat) . n - d ~ d * m + r, r < d => a + g {m} {r} = f {m+1} {r} + in divvy {n-d} {d} g + + +test :: forall (n :: Nat) . pi (m :: Nat) . Wire m Bool n Bool -> + (pi (k :: Nat) . k < 2 ^ m => Integer) +test {m} p {k} = v2i (rev (run p (toBin {m} {k}))) + + +hadd :: Wire 2 Bool 2 Bool +hadd = pipe (sequ split split) + (pipe (sequ wire (sequ cross wire)) + (sequ andGate xorGate)) + +fadd :: Wire 3 Bool 2 Bool +fadd = pipe (sequ hadd wire) + (pipe (sequ wire hadd) + (sequ orGate wire)) + + +askVec :: forall a . pi (m :: Nat) . Wire m a 1 (Vec m a) +askVec = let help :: forall a (k :: Nat) . Vec k a -> (pi (m :: Nat) . Wire m a 1 (Vec (m+k) a)) + help xs {0} = Say xs Stop + help xs {m+1} = Ask (\ x -> help (VCons x xs) {m}) + in help VNil + +sayVec :: forall a b (k :: Num) . Vec k b -> Wire 0 a k b +sayVec VNil = Stop +sayVec (VCons x xs) = Say x (sayVec xs) + +bundle2 :: forall a. pi (m :: Nat) . Wire (2*m) a 2 (Vec m a) +bundle2 {m} = sequ (askVec {m}) (askVec {m}) + +unbundle2 :: forall a . pi (m :: Nat) . Wire 2 (Vec m a) (2*m) a +unbundle2 {m} = Ask (\ xs -> Ask (\ ys -> sequ (sayVec (rev xs)) (sayVec (rev ys)))) + + +fizz = pipe (bundle2 {3}) (unbundle2 {3}) + + + +crosses :: forall a . pi (k :: Nat) . Wire (2 * k) a (2 * k) a +crosses {k} = pipe (bundle2 {k}) + (pipe cross + (unbundle2 {k})) + +crosses' :: forall a . + (forall (x y :: Nat) t . Proxy x -> Proxy y -> (0 <= x * y => t) -> t) -> + (pi (k :: Nat) . Wire (4 * k) a (4 * k) a) +crosses' lem {k} = pipe (nsequ lem {2} (bundle2 {k})) + (pipe (sequ wire (sequ cross wire)) + (nsequ lem {2} (unbundle2 {k}))) + + + +ripple :: forall a . + (forall (x y :: Nat) t . Proxy x -> Proxy y -> (0 <= x * y => t) -> t) -> + (pi (m :: Nat) . Wire (2 * 2 ^ m + 1) a (1 + 2 ^ m) a -> + Wire (2 * 2 ^ (m+1) + 1) a (1 + 2 ^ (m+1)) a) +ripple lem {m} add | {0 <= 2 ^ m} = pipe (sequ (crosses' lem {2 ^ m}) wire) + (pipe (sequ (wires {2 ^ (m+1)}) add) + (sequ add (wires {2 ^ m}))) + +adder :: (forall (x y :: Nat) t . Proxy x -> Proxy y -> (0 <= x * y => t) -> t) -> + (pi (m :: Nat) . Wire (2 * 2 ^ m + 1) Bool (1 + 2 ^ m) Bool) +adder lem {0} = fadd +adder lem {m+1} = ripple lem {m} (adder lem {m}) diff --git a/WiresExtras.hs b/WiresExtras.hs new file mode 100644 index 0000000..5b2ca73 --- /dev/null +++ b/WiresExtras.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE StandaloneDeriving, FlexibleInstances, DeriveFunctor #-} + +module WiresExtras where + +import Wires + +deriving instance Show a => Show (Vec a) +deriving instance Show (Wire Bool Bool) +deriving instance Functor Vec + +instance Show a => Show (Bool -> a) where + show f = "(True -> " ++ show (f True) ++ "; False -> " ++ show (f False) ++ ")" + +btoc True = '1' +btoc False = '0' + +ctob '0' = False +ctob '1' = True + +vtol :: Vec a -> [a] +vtol VNil = [] +vtol (VCons x xs) = x : vtol xs + +ltov :: [a] -> Vec a +ltov [] = VNil +ltov (x:xs) = VCons x (ltov xs) + +vtob = vtol . fmap btoc +btov = fmap ctob . ltov + + +lem _ _ = id + +test' m p k = vtob $ run p $ toBin m k \ No newline at end of file