Skip to content

Instantly share code, notes, and snippets.

@nrolland
Last active June 6, 2016 10:37
Show Gist options
  • Save nrolland/e6c94646775ccd6700b1c967142b9736 to your computer and use it in GitHub Desktop.
Save nrolland/e6c94646775ccd6700b1c967142b9736 to your computer and use it in GitHub Desktop.
#!/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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment