{- |
Modeling of an extensible, recursive sum datatype (recursive open union)

>  data List a = Nil | Cons a (List a)

which is later extended with two more variants,

>  ... | Unit a | App (List a) (List a)

Our goals:

  * any function that accepts the extended data list
    must also accept the unextended list.

  * it should be possible to `extend' the function that operates
    on plain lists to operate on extended list. We should be able
    to reuse as much of the old code as possible.

It seems, we have achieved our goals.

/Method/: duality rules! Curry-Howard correspondence and logic
give the wonderful guidance. In particular, we take advantage
of the fact that the deMorgan law

>     NOT (A | B) -> (NOT A & NOT B)

holds both in classical, and, more importantly, intuitionistic
logics. Our encoding of sums is the straightforward Curry-Howard
image of the law.

Note, the code below has no type classes, no type-level programming
or any other type hacking. In fact, there are no type annotations,
type declarations, or any other mentioning of types, except in the comments
-}

module Data.HList.VariantP where

import Data.HList.CommonMain
import Data.HList.Label1


-- Declare labels for extensible records -- or, dually, for
-- extensible variants
-- We used the simplest field labels. They are a bit
-- ungainly to use -- but let us avoid overlapping instance extension.
-- See OOHaskell for the use of more advanced labels.

l_nil   = firstLabel
l_cons  = nextLabel l_nil

nil consumer = consumer .!. l_nil

cons a l consumer = (consumer .!. l_cons) a (l consumer)

tl1 c = cons 'a' (cons 'b' (cons 'c' nil)) c
tl2 c = cons 10 (cons 1 (cons 2 (cons 3 nil))) c

{-
  The inferred type of tl1 is

*Variants> :t tl1
tl1 :: (HasField (Label (HSucc HZero)) r (Char -> v -> v),
        HasField (Label HZero) r v) =>
       r -> v

which basically says that tl1 accepts any consumer that has at least
fields l_nil and l_cons with appropriate types. The consumer
may have more fields
-}


-- First polymorphic function: provide a regular list "view" of our list

to_list () =     l_nil  .=. []
             .*. l_cons .=. (:)
             .*. emptyRecord

-- I wish GHC supported unicode in identifiers
tekiyou consumer lst = lst (consumer ())

test1 = tekiyou to_list tl1
-- "abc"
test2 = tekiyou to_list tl2
-- [10,1,2,3]


-- another function, length

lengthL () =  l_nil  .=. 0
          .*. l_cons .=. (\x a -> a + 1)
          .*. emptyRecord

test_lL1 = tekiyou lengthL tl1
-- 3
test_lL2 = tekiyou lengthL tl2
-- 4


-- Now, add extension to our record -- and, dually, extend our variant

l_unit = nextLabel l_cons
l_app  = nextLabel l_unit

unit a c = (c .!. l_unit) a

app l1 l2 c = (c .!. l_app) (l1 c) (l2 c)

tl3 c = cons 1 (unit 2) c
tl4 c = cons 10 (app tl3 tl2) c

sumA () =  l_nil  .=. 0
       .*. l_cons .=. (+)
       .*. l_unit .=. id
       .*. l_app  .=. (+)
       .*. emptyRecord

-- we can apply sum to an original (unextended) list
test_sum1 = tekiyou sumA tl2
-- 16

-- now, we can apply sum to an extended list
test_sum2 = tekiyou sumA tl4
-- 29

-- we can't pass extended lists tl3 and tl4 to a regular lenghtL
-- The error message says that the field l_unit is missing
-- test_lL3 = tekiyou lengthL tl3


-- now we can attempt to extend lengthL, reusing as much of previous
-- functionality as possible

lengthA () =  l_unit .=. const 1
          .*. l_app  .=. (+)
          .*. (lengthL ())

test_lL4 = tekiyou lengthA tl3
-- 2
test_lL5 = tekiyou lengthA tl4
-- 7


-- A few methods to show that our extensible lists indeed act
-- as regular lists (that is, support the regular list API).

-- check if the (extensible list) is null:
el_null l = l (l_nil .=. True .*. l_cons .=. (\_ _ -> False)
               .*. emptyRecord)

el_head l = l (l_nil .=. undefined .*. l_cons .=. (\x _ -> x)
               .*. emptyRecord)

el_tail l = l (    l_nil .=. (\f -> if f then undefined else nil)
               .*. l_cons .=. (\x a f -> if f then a False else
                               cons x (a False))
               .*. emptyRecord) True

test_ell = (el_null tl1, el_head tl1, tekiyou to_list $ el_tail tl1)


-- convert from the regular list
from_list l = foldr cons nil l

test_ft1 = tekiyou to_list $ from_list "abcd"
-- "abcd"


-- Binary methods.
-- Hmm, doing it directly is complicated. OTH, we can use the list view
-- (to_list) and solve the problem this way...
-- Laziness helps...

eqL l1 l2 = tekiyou to_list l1 == tekiyou to_list l2
test_eq1 = eqL tl1 tl1             -- True
test_eq2 = eqL tl1 (cons 'a' nil)  -- False
test_eq3 = eqL tl1 nil             -- False

-- we can extend to_list as usual

to_listA () =  l_unit .=. (:[])
           .*. l_app  .=. (++)
           .*. (to_list ())

-- And we can arbitrary mix old and extended lists
eqA l1 l2 = tekiyou to_listA l1 == tekiyou to_listA l2
test_eq4, test_eq5, test_eq6 :: Bool
test_eq4 = eqA tl1 tl1   -- True
test_eq5 = eqA tl2 tl3   -- False
test_eq6 = eqA tl3 tl4   -- False