Idris concatH via imapProperty

concath.idr

import Data.Vect
import Data.Vect.Quantifiers

%hide intersperse

-- Redefine intersperse since the prepackaged version is not
-- public export
intersperse : (sep : a) -> (xs : Vect len a) -> Vect (len + pred len) a
intersperse sep []      = []
intersperse sep (x::xs) = x :: intersperse' sep xs
  where
    intersperse' : a -> Vect n a -> Vect (n + n) a
    intersperse'         sep []      = []
    intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
                                       in sep :: x :: intersperse' sep xs

-----------------------------------------------------------

--
-- Vary the type of the thing within the container but always
-- have the same container (`Vect k`).
--

concatH : All Monoid ts => All (Vect k) ts -> HVect ts
concatH = imapProperty Monoid concat

-----------------------------------------------------------

--
-- Vary the type of the container but always have the same
-- contents (`String`).
--

vecString : Vect 2 String
vecString = ["hello ", "world"]

listString : List String
listString = ["this ", "is ", "longer"]

outputString : String
outputString =
  concat . intersperse " " . forget $ 
    imapProperty {as=[Vect ?, List]} 
                 {p=($ String)} 
                 ((, Monoid String) . Foldable) 
                 concat 
                 [vecString, listString]

outputStringPrf : Main.outputString === "hello world this is longer"
outputStringPrf = Refl

-----------------------------------------------------------

--
-- Vary the type of the container but always have the same
-- contents (`a`).
--

concatH' : {a : _} 
       -> {as : Vect _ _}
       -> All ((, Monoid a) . Foldable) as => 
             All ($ a) as
          -> All (const a) as
concatH' = imapProperty ((, Monoid a) . Foldable) concat

outputString2 : String
outputString2 =
  concat . intersperse " " . forget $ 
    concatH' {as=[Vect ?, List]} [vecString, listString]

outputString2Prf : Main.outputString2 === "hello world this is longer"
outputString2Prf = Refl

-----------------------------------------------------------

--
-- Vary the type of the container and contents.
--

||| `imapProperty` but explicitly passing the constraint to the function being
||| mapped over the `All` rather than auto-implicitly.
imapProperty' : {0 a : Type}
             -> {0 p,q : a -> Type}
             -> (0 i : a -> Type)
             -> (f : {0 x : a} -> i x -> p x -> q x)
             -> {0 as : Vect n a}
             -> All i as => All p as -> All q as
imapProperty' _ _              []      = []
imapProperty' i f @{ix :: ixs} (x::xs) = (f ix x) :: (imapProperty' i f @{ixs} xs)

%unbound_implicits off

||| Apply a property of an `All` to produce a new
||| `All` with the property `Prelude.id`.
public export
apply : {0 l : Nat}
    -> {0 a : Type } 
    -> {0 xs : Vect l a}
    -> {f : a -> Type}
    -> All f xs
    -> All id (map f xs)
apply {f} [] = []
apply {f} (x :: y) = x :: apply {f} y

public export
0 fnToType : {l : Nat} -> Vect l Type -> Vect l Type
fnToType [] = []
fnToType (x :: xs) = (x -> Type) :: (fnToType xs)

%unbound_implicits on
public export
data Constraints : {constraintInputShapes : Vect l Type} 
                -> (constraintTys : All Prelude.id (fnToType constraintInputShapes))
                -> (tys : All Prelude.id constraintInputShapes)
                -> Type where
  Nil  : Constraints [] []
  (::) : {0 cis : Type} -> {0 cty : cis -> Type} -> {0 ty : cis} -> cty ty
      -> Constraints {constraintInputShapes} constraintTys tys 
      -> Constraints {constraintInputShapes = cis :: constraintInputShapes} (cty :: constraintTys) (ty :: tys)
%unbound_implicits off

testSearch : Constraints [Foldable, Monoid] [List, String]
testSearch = %search

||| The shape of constraints for a container (e.g. List)
||| and the type of thing within it.
|||
||| For example, [Foldable, Monoid] describes the container
||| as Foldable and the contents of the container as Monoidal.
0 Container : Type
Container = All id [(Type -> Type), Type]

ContainerContentType : Container -> Type
ContainerContentType [_, y] = y

ContainerType : Container -> Type
ContainerType [x, y] = x y

concatH'' : {0 l : Nat}
         -> {0 as : Vect l Container}
         -> All (Constraints [Foldable, Monoid]) as => 
               All ContainerType as
            -> All ContainerContentType as
concatH'' =
  imapProperty' (Constraints [Foldable, Monoid]) 
                (\[f, m] => Prelude.concat)

listNat : List Nat
listNat = [1, 2, 3]

vecString2 : Vect 4 String
vecString2 = ["hello ", "world. ","welcome ", "sun"]

output3 : All id [String, Nat]
output3 =
  let m = Num.Monoid.Additive
  in  apply $ concatH'' {as=[[Vect ?, ?], [List, ?]]} [vecString, listNat]

output3Prf : output3 === ["hello world", 6]
output3Prf = Refl

-----------------------------------------------------------

--
-- One constraint on container and two on contents.
--

concatShow : {0 l : Nat}
         -> {0 as : Vect l Container}
         -> All (Constraints [Foldable, (\t => (Monoid t, Show t))]) as => 
               All ContainerType as
            -> All (const String) as
concatShow =
  imapProperty' (Constraints [Foldable, (\t => (Monoid t, Show t))]) 
                (\[f, m] => Prelude.show . Prelude.concat)

output4 : All id [String, String]
output4 =
  let m = Num.Monoid.Additive
  in  apply $ concatShow {as=[[Vect ?, ?], [List, ?]]} [vecString, listNat]

{-
-- The following is roughly true. You can evaluate `output4` to see it.
-- It only doesn't work at compile time because the compiler gets stuck on
-- a primitive function or two.
output4Prf : output4 === ["\"hello world\"", "6"]
output4Prf = Refl
-}