It seems like you're doing a really good job cleaning up the puppet code base :) while enabling having values as types, like Integer[1,0x10] specifying an integer between 1 and 16. It looks like you're starting to add dependent types to puppet (thumbs up!).
In its core I want to use Puppet as a declarative specification system. Type systems are also declarative specifications and to me it seems a lot of the work you're doing on types means tooling like puppet lint and Geppetto will get stronger and catch more errors ahead of time.
It's worth considering more than values that represent primitives, regexes or hashes, imo. Since puppet is a configuration management tool and not a general programming language, I think it would be nice to have types that can specify security properties or protocols (finite state machines) that interact with resources or things that facilitate coordination between nodes initialising such as monotonic counters with auto-creating 'requires'-relationships to other nodes running.
In terms of security properties, perhaps it would be useful to create type-values for firewall rules or authorisation rules.
In terms of protocols, a common pattern: find a resource, download it, extract tarball, compile, install, run service of. It can be seen as a one-time run 'refreshonly' of a state-machine, each step requiring possibly a compensating step or different policies on failure for retry. This is basically a Saga in distributed system parlance and you could tie this into what's going on with etcd by letting a protocol like Raft provide the foundation for a distributed replicated state machine fed from a replicated log that each cohort (Raft-running node) agrees on -- the saga's state parameter equals the last agreed operation of the Raft-log.
In terms of syntax you could also study what makes Bloom lang really good at describing distributed computation in a way that's fairly non-imperative. Of course, if you read up on Bloom, don't miss conflict-free replicated data types and how commutative+associative functions can be nicely used to write eventually consistent data types/structures.
Further, because protocols, state machines and sequencing of operations is really such a core business for any computer system provisioning, let me link to the yield paper and Ekmett's implementation of yield. It provides four core values: (data Plan = Done a | Yield o (Plan k o a) | forall z. Await (z -> Plan k o a) (k z) (Plan k o a) | Fail) which lets you put together plans at a type level (albeit with opaque functions doing the work, but those could be typed perhaps?) which you can analyse, compile and use together with a state-carrying monad. Perhaps machines for v5? :)
The primary use-case I find for using undef in puppet code is when negating set properties of declared resources. This could be solved with discriminated union types also (like the one you saw above for machines) -- they are very powerful in reducing cyclomatic complexity, a very dangerous maintenance metric that puppet-code suffers often suffers from. Perhaps combining them with declarative state machines and we can declare both commission and de-commission from the same place without resorting to monstrosities like unless $enabled = true { Service['mysvc'] -> Package ... } and a contrary clause in the enabled case where service starts last. Just look at purpleidea
You would probably enjoy reading up a bit on F# and F* -- it's a powerful language, especially the extensions. It's been used to prove a TLS implementation for example (http://www.mitls.org/wsgi/), F# is apache licensed and runs well on linux, and the implementation in F7 referenced above (precursor to F*) has a lot of the declarative and dependent types you seem to be gravitating towards implemented.
Yes, the types are dependent types (A challenge is making computer science easy to understand and easy to use by the typical Puppet user. Hence the lack of more in-depth type-theory in the blog posts.)
While I have not thought so much about orchestration and executing plans in terms of the type system I think that (state-machine / petri-net) is where Puppet needs to go to enable running a "global catalog" (a distributed state machine backed by something Raft like - if not Raft itself). When doing so there will clearly be reusable "plan parts", that could be represented by Type. At first, the planning and orchestration is probably not going to be exposed in any fancy way in the Puppet Language, but to be really useful (as you point out) it really needs to be. It may be implemented in a revised Resource Type layer and thus something used by the more advanced users). Maybe something emerges during 2014, at present I have only started on a minimalistic implementation (to understand the issues better). But first things first, cleaning up the core of the language, untangling everything...
Thanks for all the pointers to interesting reading.