functional unparsing as in Danvy - https://cs.au.dk/~danvy/DSc/16_danvy_jfp-1998.pdf

AP1Functional_unparsing_by_Danvy.hs

#!/usr/bin/env stack
-- stack --resolver lts-17.10 script

-- or
-- stack --install-ghc --resolver lts-17.10 runghc --package base-unicode-symbols
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}

module AP1Functional_unparsing_by_Danvy 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' :: forall c. (String -> c) -> String -> Int -> Int -> c
t' (k :: String -> c) =
  -- 3. j'applique int au type a ~ (Int → c)
  (int :: forall a. (String -> a) -> String -> Int -> a)
    ( -- 1. j'applique int au type b  ~ c
      (int :: forall 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

exemple1 :: Int -> Int -> String
exemple1 =
  (format :: forall a. ((String -> String) -> String -> a) -> a) -- applique en a = Int -> Int → Sting
    (t :: forall 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"

main :: IO ()
main = print v

---- 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 ""

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

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

exemple3 :: (Int, String) -> Int -> String
exemple3 = format' $ (formatK (PInt ⊗ PString)) ∘ (formatK PInt)

exemple4 =
  format'
    $( (formatK PInt :: (String -> (Int -> String)) -> String -> Int -> (Int -> String))
         ∘ (formatK PInt :: (String -> String) -> String -> (Int -> String)) ::
         (String -> String) -> String -> Int -> Int -> String
     )

exemple5 = format' $ (formatK PInt) ∘ (formatK PInt)