Part2_Sez10_1_views

Markdown generated from:
Source idr program: /src/Part2/Sez10_1_views.idr
Source lhs program: /src/Part2/Sez10_1_views.lhs

using 'z' in the name to recover alphabetical sort of sections

Section 10.1 Idris ListLast, SplitList, TakeN views vs Haskell

Pattern matching using views. Idris allows for a very expressive pattern match informed by GADT-like structures.
Haskell does not and the GADTs need to be used directly in the pattern match. Well, there is the ViewPatterns pragma, which I am using here, but I am not very happy about it (see Slow reverse example below). Also, Haskell GADTs need to contain more information, while Idris can infer (or, rather, exfer) such information.
Idris is capable of matching on the type (RHS) of constructor. This extends the traditional matching on the constructor itself (LHS).

I ended up using SomeSing in the return type and I am testing with Nat data trying to avoid complexity of using literals in dependently typed Haskell code. My Haskell examples use singletons.

Idris code example

{- using 'z' in file name to recover alphabetical sort -}
module Part2.Sez10_1_views 

%default total 

{- ListLast view examples -}
data ListLast : List a -> Type where 
   Empty : ListLast [] 
   NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
      Empty => NonEmpty [] x
      NonEmpty ys y => NonEmpty (x :: ys) y


describeHelper : (input : List Int) -> ListLast input -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x)
        = "Non-empty, initial portion = " ++ show xs

describeListEnd : List Int -> String
describeListEnd xs = describeHelper xs (listLast xs)

{- cool with syntax adds additional arguments to function implementation -}
describeListEnd' : List Int -> String
describeListEnd' input with (listLast input)
  describeListEnd' [] | Empty = "Empty"
  describeListEnd' (xs ++ [x]) | (NonEmpty xs x)
          = "Non-empty, initial portion = " ++ show xs

|||slow reverse - ListLast view is rebuilt in each recursive step
covering
myReverse : List a -> List a
myReverse input with (listLast input)
    myReverse [] | Empty = []
    myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs

{- 
idris repl:
*Part2/Sez10_1_views> myReverse [5,2,7,1]
[1, 7, 2, 5] : List Integer
-}

{- SplitList, merge sort example -}
data SplitList : List a -> Type where
     SplitNil : SplitList []
     SplitOne : SplitList [x]
     SplitPair : (lefts : List a) -> (rights : List a) ->
                 SplitList (lefts ++ rights)

total
splitList : (input : List a) -> SplitList input
splitList input = splitListHelp input input
where
  {- the first list acts as a counter only, 
     each step removes 2 elements from the counter and adds new elements to `lefts` 
     when counter is excausted all elements are added to `rights` -}
  splitListHelp : List a -> (input : List a) -> SplitList input
  splitListHelp _ [] = SplitNil
  splitListHelp _ [x] = SplitOne
  splitListHelp (_ :: _ :: counter) (item :: items)
       = case splitListHelp counter items of
              SplitNil => SplitOne  --cool how Idris figures this out!
              SplitOne {x} => SplitPair [item] [x]
              SplitPair lefts rights => SplitPair (item :: lefts) rights
  splitListHelp _ items = SplitPair [] items

covering
mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
   mergeSort [] | SplitNil = []
   mergeSort [x] | SplitOne = [x]
   mergeSort (lefts ++ rights) | (SplitPair lefts rights)
                 -- merge : Ord a => List a -> List a -> List a
                 = merge (mergeSort lefts) (mergeSort rights)

{-
idris repl: 
*Part2/Sez10_1_views> mergeSort [5,2,7,1]
[1, 2, 5, 7] : List Integer
-}

-- excercises
data TakeN : List a -> Type where
      Fewer : TakeN xs
      Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)
         
takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []  --kinda amazing how much Idris infers here!
takeN (S k) [] = Fewer 
takeN (S k) (x :: xs) = case takeN k xs of 
       Fewer => Fewer
       Exact rxs => Exact (x :: rxs)

covering
groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

{-
idris repl:
*Part2/Sez10_1_views> groupByN 3 [1..10]
[[1, 2, 3], [4, 5, 6], [7, 8, 9], [10]] : List (List Integer)
-}

-- excercise 2
-- use of div forces `partial` here
partial
halves : List a -> (List a, List a)
halves list with (takeN ((length list) `div` 2) list)
   halves list | Fewer = (list, [])
   halves (half1 ++ half2) | (Exact half1) = (half1, half2)

{-
*Part2/Sez10_1_views> halves [1..10]
([1, 2, 3, 4, 5], [6, 7, 8, 9, 10]) : (List Integer, List Integer)
*Part2/Sez10_1_views> halves [1]
([], [1]) : (List Integer, List Integer)
*Part2/Sez10_1_views> the (List Integer, List Integer) (halves [])
([], []) : (List Integer, List Integer)
-} 

Compared to Haskell

{-# LANGUAGE 
   TemplateHaskell
   , TypeOperators
   , GADTs
   , TypeFamilies
   , DataKinds
   , PolyKinds
   , KindSignatures
   , EmptyCase
   , RankNTypes
   , LambdaCase
   , ScopedTypeVariables 
   , FlexibleContexts
   , ViewPatterns
#-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Part2.Sez10_1_views where
import Data.SingBased.Nat (Nat(..), type Sing(..), integerToNat, natToInteger, sHalf)
import Data.SingBased.List (List(..), type Sing(..))
import qualified Data.SingBased.List as L
import qualified Part2.Sec8_3_deceq as P
import Data.Singletons
import Data.Bifunctor (bimap)

describeList example

data ListLast  (xs :: List a) where 
   Empty :: ListLast 'LNil 
   NonEmpty :: forall (xs :: List a) (x :: a). 
               Sing xs -> Sing x -> ListLast (L.Append xs (L.OneElem x))

listLast :: forall (xs :: List a) . Sing xs -> ListLast xs
listLast SLNil = Empty
listLast (x `SLCons` xs) = case listLast xs of
      Empty -> NonEmpty SLNil x
      NonEmpty ys y -> NonEmpty (SLCons x ys) y

describeHelper1 :: forall (input :: List a) . (SingKind a, Show (Demote a)) => 
                    Sing input -> ListLast input -> String
describeHelper1 SLNil Empty = "Empty"
describeHelper1 _ (NonEmpty xs x) = "Non-empty, initial portion = " ++ (show $ fromSing xs)

describeHelper2 :: forall (xs :: List a) . (SingKind a, Show (Demote a)) => 
                    Sing xs -> String
describeHelper2 xs = describeHelper1 xs (listLast xs)

describeListEnd :: (SingKind a, Show (Demote a)) => List (Demote a) -> String
describeListEnd list = withSomeSing list describeHelper2

Int does not have the boilerplate needed by singletons, I use Nat to test it

test :: List Nat
test =  Z `LCons` (S Z) `LCons` LNil

describeListNat :: List Nat -> String
describeListNat = describeListEnd

ghci

*Part2.Sez10_1_views> describeListEnd test
"Non-empty, initial portion = LCons Z LNil"

Slow reverse example

I am using ViewPatterns here (see myReverseHelper listLast -> ... syntax).
I am not using this extension elsewhere. It appears that with GHC 8.2.2 this extension does not play well with -fwarn-incomplete-patterns.

myReverseHelper :: forall (xs :: List a) . Sing xs  -> SomeSing (List a)
myReverseHelper (listLast -> Empty) = SomeSing SLNil 
myReverseHelper (listLast -> (NonEmpty xs x)) = case myReverseHelper xs of
             SomeSing sres -> SomeSing $ SLCons x sres 
myReverseHelper _ = error "ViewPatterns do not know that pattern match is exhaustive" 

myReverse :: (SingKind a) => List (Demote a) -> List (Demote a)
myReverse list = case withSomeSing list (\xs ->  myReverseHelper xs) of 
                   SomeSing res -> fromSing res

testWithList :: [a] -> (a->b) -> (List b -> List c) -> (c->d) -> [d]
testWithList al fab flist fcd 
       = map fcd $ L.listToL $ flist $ L.lToList (map fab al)

ghci

*Part2.Sez10_1_views> testWithList [4,2,7,1] integerToNat myReverse natToInteger
[1,7,2,4]

Note, I have to use SomeSing (List a) as return type when defining myReverseHelper or similar type level list operations. Returning Sing xs would imply that the returned list is exactly the same as Sing xs input.
For example, this works

myTail :: forall (xs :: List a) . Sing xs -> SomeSing (List a)
myTail SLNil = SomeSing SLNil 
myTail (SLCons x xs) = SomeSing xs

but this makes no sense and does not compile:

myTail :: forall (xs :: List a) . Sing xs -> Sing xs
myTail SLNil = SLNil 
myTail (SLCons x xs) = xs -- compilation problem

mergeSort example

data SplitList (xs :: List a) where
    SplitNil :: SplitList 'LNil
    SplitOne :: Sing x -> SplitList (L.OneElem x)
    SplitPair :: forall (lefts :: List a) (rights :: List a). 
                Sing lefts -> Sing rights ->
                SplitList (L.Append lefts rights)

-- used for testing only:
testSplitList :: forall (xs :: List a). SingKind a => SplitList xs -> [List (Demote a)]
testSplitList SplitNil = [LNil]
testSplitList (SplitOne x) = [L.oneElem (fromSing x)]
testSplitList (SplitPair xs ys) = [fromSing xs, fromSing ys]

splitList :: forall (input :: List a). SingKind a => Sing input -> SplitList input
splitList input = splitListHelp (fromSing input) input

splitListHelp :: forall (input :: List a). SingKind a => 
                  List (Demote a) -> Sing input -> SplitList input
splitListHelp _ SLNil = SplitNil
splitListHelp _ (SLCons x SLNil) = SplitOne x
splitListHelp (_ `LCons` _ `LCons` counter) (item `SLCons` items) 
      = case splitListHelp counter items of
            SplitNil -> SplitOne item
            SplitOne x ->  SplitPair (L.sOneElem item) (L.sOneElem x)
            SplitPair lefts rights ->  SplitPair (item `SLCons` lefts) rights
splitListHelp _ items = SplitPair SLNil items

ghci:

*Part2.Sez10_1_views> testSplitList $ splitList $ s0 `SLCons` s0 `SLCons` s1 `SLCons` s1 `SLCons` SLNil
[LCons Z (LCons Z LNil),LCons (S Z) (LCons (S Z) LNil)]

Unfortunately the standard merge function (see Data.SingBased.List) does not lift easily with singletons. SomeSing needs to be used in the result type, again, to make it work

sMerge :: forall (xs :: List a) (ys :: List a). (SingKind a, Ord (Demote a)) => 
           Sing xs -> Sing ys -> SomeSing (List a)
sMerge list1 list2 
      = let xres = L.merge (fromSing list1) (fromSing list2)
        in toSing xres

mergeSort :: (SingKind a, Ord (Demote a)) => List (Demote a) -> List (Demote a)
mergeSort list = case withSomeSing list (\xs -> mergeSortHelper (splitList xs) xs) of
          SomeSing res -> fromSing res

mergeSortHelper :: forall (xs :: List a). (SingKind a, Ord (Demote a)) => 
                    SplitList xs -> Sing xs -> SomeSing (List a)
mergeSortHelper SplitNil SLNil = SomeSing SLNil
mergeSortHelper (SplitOne x) _ = SomeSing (L.sOneElem x)
mergeSortHelper (SplitPair lefts rights) _ 
    = case mergeSortHelper (splitList lefts) lefts of 
        SomeSing leftsRes -> case mergeSortHelper (splitList rights) rights of
          SomeSing rightsRes -> sMerge leftsRes rightsRes 

testSort = testWithList [4,2,5,1] integerToNat mergeSort natToInteger

ghci

*Part2.Sez10_1_views> testSort
[1,2,4,5]

Exercises

I managed to get close to the Idris' TakeN definition. I added an explicit rest argument to the Exact constructor.

data TakeN (xs :: List a) where
     Fewer :: TakeN xs
     Exact :: Sing n_xs -> Sing rest -> TakeN (L.Append n_xs rest)

takeN ::  forall (n :: Nat) (xs :: List a) . Sing n -> Sing xs -> TakeN xs
takeN SZ xs = Exact SLNil xs 
takeN(SS k) SLNil = Fewer
takeN (SS k) (x `SLCons` xs) = case takeN k xs of 
      Fewer -> Fewer
      Exact rxs rest ->  Exact (x `SLCons` rxs) rest

Trying to get even closer to Idris requires AllowAmbiguousTypes:

data TakeN_ (xs :: List a) where
      Fewer_ :: TakeN_ xs
      Exact_ :: Sing n_xs -> TakeN_ (L.Append n_xs rest)

and I had hard time convincing ghc to compile takeN_ implemented based on that definition (TODO).

groupByNHelper :: forall (n :: Nat) (xs :: List a) . 
                  Sing n -> 
                  Sing xs -> SomeSing (List (List a))
groupByNHelper n xs = case takeN n xs of 
          Fewer -> SomeSing (L.sOneElem xs)
          Exact n_xs rrest -> case groupByNHelper n rrest of
                   SomeSing n_next -> SomeSing $ n_xs `SLCons` n_next

groupByN :: (SingKind a) => Nat -> List (Demote a) -> List ( List (Demote a))
groupByN n list = case withSomeSing n (\sn -> withSomeSing list $ groupByNHelper sn ) 
      of SomeSing res -> fromSing res

testGroup = testWithList [1..10] integerToNat (groupByN (integerToNat 3)) (map natToInteger . L.listToL) 

ghci:

*Part2.Sez10_1_views> testGroup
[[1,2,3],[4,5,6],[7,8,9],[10]]

halvesHelper :: forall (xs :: List a) . Sing xs -> SomeSing (P.MyPair (List a) (List a))
halvesHelper slist 
       = case takeN (sHalf $ L.sLLength slist) slist of
           Fewer -> SomeSing $ P.SMkMyPair slist SLNil
           Exact xs ys -> SomeSing $ P.SMkMyPair xs ys

halves :: (SingKind a) => List (Demote a) -> P.MyPair (List (Demote a)) (List (Demote a))
halves list = case withSomeSing list halvesHelper of 
       SomeSing res -> fromSing res

testHalves =  let convert = map natToInteger . L.listToL
              in bimap convert convert . halves . L.lToList . map integerToNat 

ghci:

*Part2.Sez10_1_views> testHalves [1..10]
MkMyPair [1,2,3,4,5] [6,7,8,9,10]
*Part2.Sez10_1_views> testHalves [1]
MkMyPair [] [1]
*Part2.Sez10_1_views> testHalves []
MkMyPair [] []