dependent types - Type Theory

I may be just starting to understand where dependent types could be useful but am unsure if this is actually an example of them. Is the following an example of dependent types composeFold :: [a -> b, c -> d, ..., y -> z] -> a -> z? If that type doesn't make sense, composeFold is a function that takes a list of functions and composes them into a function that takes the argument type of the first function in the list and returns the return type of the last function in the list. Somehow, the static type checker would have to ensure that only a list of composable functions is constructed.

I find it funny how new type ideas start springing out at me when I start programming some JavaScript again because of how free flowing and unsafe the language is.

JavaScript awful for programming but amazing for coming up with strange new type usages that need to be formalized

Maybe one way to think about practical application of dependent types is that they can encode things usually represented by predicates - e.g. proof that value is element of some container, or list has length equal to something etc.
In those cases where you use if and assume some fact in some of it's branches, you can often come up with actual proofs that you can pass down to functions in those branches in languages with DT. They don't magically make dynamic problems static - instead, they let you reason about dynamic information in safe way, prohibiting you from making wrong assumptions

BTW, your example is usually represented by special list defined as GADT:

data ComposeList a b where
  CNil :: ComposeList a a
  CCons :: (a -> b) -> ComposeList b c -> ComposeList a c

technically you could do something like this too if you want to match on specific pipelines:

data CList :: [Type] -> Type where
  CNil :: ComposeList '[a, a]
  CCons :: (a -> b) -> ComposeList (b':l) -> ComposeList (a':b':l)

though I'm not sure where it would be useful

I was looking at compiler pipelines and being able to switch compiler components without recompiling. Example trying different combinations of optimizers. Or being able to switch frontends to add a different programming language.

The GADT is a cool way to accomplish this.

What you describe sounds like a good fit for simple record - one where elements are functions handling specific parts of pipeline