I've decided that it's the same as having a simply-typed lambda calculus with one type (*) and function types living inside of your type system. Is this correct at all?