From 2569812bcc065198509355d4c269dd9539ed6a7a Mon Sep 17 00:00:00 2001 From: Robert Atkey Date: Wed, 10 Aug 2011 13:59:55 +0100 Subject: [PATCH] Some fiddling with the replaceMin example --- experiments/DelayIdiomNBE.hs | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/experiments/DelayIdiomNBE.hs b/experiments/DelayIdiomNBE.hs index 45d3106..6013a5d 100644 --- a/experiments/DelayIdiomNBE.hs +++ b/experiments/DelayIdiomNBE.hs @@ -166,8 +166,25 @@ replaceTm = (Pair (Pure fstFunc `Ap` (Var 1 `Ap` Pure (Var 0))) (Pure fstFunc `Ap` (Var 1 `Ap` Pure (Var 0)))) +-- \f p. (min (fst p) (snd p), ( fst <$> (f <*> pure y) +-- , fst <$> (f <*> pure y))) + +fix f = f (fix f) + +letrec :: ((a,s) -> (b,s)) -> a -> b +letrec f a = let (b,s) = f (a,s) in b + +letrec' :: ((a,s) -> (b,s)) -> a -> b +letrec' f a = fst (fix (\h a -> f (a, snd $ h a)) a) + +f ((x,y), s) = ((s,s), min x y) + replaceMinTm = Lam (B :*: B) (Snd (Fix replaceTm `App` Var 0)) replaceMinTy = (B :*: B) :=> (De B :*: De B) -xTm = Lam (B :*: B) (Force B (Fst (replaceMinTm `App` Var 0))) -xTy = (B :*: B) :=> B +xTm = Lam (B :*: B) + (Let (De B :*: De B) + (replaceMinTm `App` Var 0) + (Pair (Force B (Fst (Var 0))) + (Force B (Snd (Var 0))))) +xTy = (B :*: B) :=> (B :*: B)