functional unparsing by Danvy.hs

#!/usr/bin/env stack
-- stack --install-ghc --resolver lts-6.1 runghc --package http-conduit
{-# LANGUAGE InstanceSigs, FlexibleInstances, KindSignatures, TypeFamilies, LambdaCase  #-}
{-# LANGUAGE OverloadedStrings, RankNTypes, MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, PartialTypeSignatures #-}
module MainFunctionalUnparsing where

import Data.Proxy
import Prelude.Unicode

-- http://www.brics.dk/RS/98/12/BRICS-RS-98-12.pdf

-- we use continuation-passing style (CPS) to thread the constructed string
-- throughout. We also exploit the polymorphic domain of answers to instantiate
-- it to the appropriately typed function


-- Abstract syntax of patterns:
-- The data type of patterns is composed of the following pattern directives:
-- • lit for declaring literal strings (" is " and "/" above);
-- • eol for declaring newlines (%n above);
-- • int for specifying integers (%i above); and
-- • str for specifying strings (%s above).

-- a gauche => on fournit maintenant, a droite ⇒ on fournira plus tard
lit ∷  String -> (String -> a) -> String -> a
lit x k s = k (s ++ x)

eol ∷  (String -> a) -> String -> a
eol k s = k (s ++ "\n")

int ∷ (String -> a) -> String -> Int -> a
int k s x = k (s ++ show x)

str ∷ (String -> a) -> String -> String -> a
str k s x = k (s ++ x)

-- C'est la Magie !
t :: (String -> a) -> String -> Int -> Int -> a
t = int ∘ int

-- examinons bien ca :
-- int est polymorphe
t' :: ∀ c. (String -> c) -> String -> Int -> Int -> c
t' (k ∷ String -> c)  =
  -- 3. j'applique int au type a ~ (Int → c)
  (int ∷ ∀a.  (String -> a) -> String -> Int -> a)
    ( -- 1. j'applique int au type b  ~ c
      (int ∷ ∀b.  (String -> b) -> String -> Int -> b) (k ∷ String -> c)
      ∷ String -> Int -> c -- 2. j'ai donc un type String → (Int → c)
    ) ∷  String -> Int -> Int -> c -- 4. j'ai donc un type String → Int → Int → c

-- on ferme le type avec
format ∷ ((String -> String) -> String -> a) -> a
format p = p (id ∷ String → String) ("" ∷ String)

-- ∀ r.  r ≡ ∀ s . (r → s) → s

exemple :: Int -> Int -> String
exemple = (format ∷ ∀ a .((String -> String) -> String -> a) -> a) -- applique en a = Int -> Int → Sting
              (t∷ ∀ r . (String -> r) -> String -> Int -> Int -> r) -- applique en r = String

exemple2 :: Int -> String -> String
exemple2 = format (int .  lit " is " . str . eol)

v = exemple2 3 "odd"


---- avec GADT, les constructeurs fixent le type rajoute
-- a l'inverse du functional unparsing on ne manipule pas la semantique mais on construit un terme (shallow vs deep)
-- avec du type level on associerait de la meme maniere un type a nos data contructeur
data Pattern ∷ * → * where
  PInt ∷ Pattern Int
  PString ∷ Pattern String
  PPair ∷ (Pattern a, Pattern b) → Pattern (a,b)

-- ce qui nous force a interpreter
formatK ∷ Pattern a → (String → b) → String → a → b
formatK PInt k s i = k( s Prelude.++ show i)
formatK PString k s sa = k( s Prelude.++ sa)
formatK (PPair (a1, a2)) (k ∷ String → b) s (va1,va2) =
  formatK a1 (\sa1 → formatK a2 k sa1 va2) s va1

format ∷ ((String → String) → String → b) → b
format p = p id ""

-- one ne peut pas composer comme dans le papier originel
(**) x y = PPair (x,y)

-- (f ∘ g) k = f (g k)

exemple1 :: (Int, String) -> Int -> String
exemple1 = format $ (formatK (PInt ** PString)) . (formatK PInt)
exemple2 = format $((formatK PInt ∷ (String → (Int → String)) → String → Int → (Int → String))
                      . (formatK PInt ∷ (String → String) → String → (Int → String))
                     ∷ (String → String) -> String → Int → Int → String)
exemple3 = format $ (formatK PInt) . (formatK PInt)