Dhall folding types

experiment.dhall

let default_list = https://prelude.dhall-lang.org/List/default

let combiner 
    : forall ( T : Type ) -> forall ( default : T ) -> forall ( combine : T -> T -> T ) -> ( T -> T -> T )
    = 
    \( T : Type ) -> \( default : T ) -> \( combine : T -> T -> T ) ->
        \( left : T ) -> \( right : T ) ->
            -- The following expression is what would make this work but unfortunaly it doesn't for
            -- it seems that to make this work something called row polymorphism is needed. The error
            -- you'd get when running this is the compiler saying the types of left and right are not
            -- T but are "Type" to bad really.
            --
            -- As a work around we're doing the entire combine in the combiner callback
            -- 
            -- ( default // left // right // combine left right ) : T
            --
            -- I think for the same reasons providing the type record instead of the type doesn't work
            -- either. I think it would look something like this and would seem rather ergonomic
            --
            --  \( T : RecordType ) -> \( combine : T -> T -> T ) ->
            --      \( left : T ) -> \( right : T ) ->
            --          T::{=} // left // right // combine left right
            --
            ( combine left right ) : T

let folder 
    : forall ( T : Type ) -> forall ( combiner : T -> T -> T ) -> ( List T -> T -> T )
    = 
    \( T : Type ) -> \( combiner : T -> T -> T ) ->
        \( mixins : List T ) -> \( target : T ) ->
            List/fold T mixins T combiner target

let T_type = {
    text : Optional Text,
    list : Optional ( List Text )
}

let T_default = {
    text = None Text,
    list = None ( List Text )
}

let T_combine = combiner T_type T_default ( 
    
    \( left : T_type ) -> \( right : T_type ) -> 
        ( 
        
            T_default
            // left
            // right
            // { list = Some ( default_list Text left.list # default_list Text right.list ) }
        
        ) : T_type

)

let T_fold = folder T_type T_combine

let T = {
    , Type    = T_type
    , default = T_default
    , combine = T_combine
    , fold    = T_fold
}

in {
    
    , first = T::{
        text = Some "first text",
        list = Some [ "first", "third" ]
    }

    , second = T::{=}
        // { text = Some "Second text" }
        // { list = Some [ "nope" ] }
        // { list = Some [ "override not append" ] }

    , third = T.combine
        T::{ text = Some "left text", list = Some [ "prefix" ] }
        T::{ text = Some "right text", list = Some [ "suffix" ] }

    , forth = T.fold
        [ T::{ list = Some [ "first" ] }
        , T::{ list = Some [ "second" ] }
        , T::{ list = Some [ "third" ] }
        ]
        T::{ text = Some "Folding space and time", list = Some [ "For science!" ] }
}