Created
April 28, 2021 06:18
-
-
Save nrolland/a282bb040bdac229baf36742ae425bc0 to your computer and use it in GitHub Desktop.
functional unparsing as in Danvy - https://cs.au.dk/~danvy/DSc/16_danvy_jfp-1998.pdf
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment