On 27 June 2010 19:14, Max Bolingbroke
I'm going to try for normalisation of Lindleys idiom calculus now.
Made me sweat, but I got it to work. From "Thingy" you get a free one-pass normaliser for idioms. Is this a novel result? It's certainly very cool! Term language: \begin{code} type Term = String data IdiomSyn = Pure Term | Ap IdiomSyn IdiomSyn | Foreign String \end{code} The normalisation algorithm: \begin{code} normalise :: IdiomSyn -> IdiomSyn normalise m = go m (\tt -> Pure (tt "id")) id where -- i a -> forall b. (forall c. ((a -> b) -> c) -> i c) -> (forall d. (b -> d) -> i d) go :: IdiomSyn -> ( (Term -> Term) -> IdiomSyn) -> ( (Term -> Term) -> IdiomSyn) go (Pure x) m = \k -> m (k . (\t -> t ++ " (" ++ x ++ ")")) go (Ap mf mx) m = go mx (go mf (\k -> m (k . (\t -> "(.) (" ++ t ++ ")")))) go (Foreign e) m = \k -> m (\t -> "(.) (\\x -> " ++ k "x" ++ ") (" ++ t ++ ")") `Ap` Foreign e \end{code} As before, we get Pure and Ap for free from Thingy if we just unfold the uses of the Yoneda "fmap" like so:
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> Yoneda i b }
instance Applicative (Thingy i) where pure x = Thingy $ \m -> Yoneda (\k -> runYoneda m (k . ($ x))) mf <*> mx = Thingy $ \m -> runThingy mx (runThingy mf (Yoneda (\k -> runYoneda m (k . (.)))))
It is fairly easy to see how they relate. The "Foreign" rule was tricky, and I derived the correct form by following the types (please pardon my lack of variable hygiene too!). Here are some examples that show how we can derive the applicative normal forms of a few terms, in exactly the form that I remembered from Wallace's Flatpack presentation: """ == Before launchMissiles <*> (obtainLaunchCode <*> (getAuthorization)) == After pure ((.) (\x -> (.) (\x -> (.) (\x -> x) (x)) ((.) (x))) ((.) (id))) <*> (launchMissiles) <*> (obtainLaunchCode) <*> (getAuthorization) == Before pure (launchMissiles') <*> (pure (obtainLaunchCode') <*> (pure (getAuthorization'))) == After pure ((.) ((.) (id) (launchMissiles')) (obtainLaunchCode') (getAuthorization')) == Before pure (f) <*> (pure (x)) == After pure ((.) (id) (f) (x)) == Before launchMissiles <*> (pure (1337)) == After pure ((.) (\x -> x (1337)) ((.) (id))) <*> (launchMissiles) """ Pretty awesome! Perhaps I should write a paper or at least a coherent note on this topic :-) Cheers, Max