This project is an experiment in bringing dependent types to F#. Dependent typing makes supporting a finer level of type granularity easier.
This library presents two alternate generic dependent types. One taking an input element to the same base type within the dependent type
'T -> 'T, and the other
taking the input type to a new base type
'T1 -> 'T2. Dependent types support the same equality and comparison traits as their base type
'T2). Extension methods are not yet supported.
The core dependent type
relies on a "constructor" type
which in turn requires a function
'Config -> 'T1 -> 'T2 option that validates the input element. Another type handles consuming the
In practice the construction of a family of dependent types looks like this:
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22:
The full validation function
regExStringVerifyis not shown.
The presence of
module DigitsDefis strictly for readability purposes, segregating the "helper" functions and types.
- All the helper types must have the same access level as the dependent type.
- Aliasing is optional, but obviously provides better readability.
Cctoris not really a constructor.
With possible changes to the F# language, the intervening
'Configconsuming helper type may be superfluous.
Alternately, a dependent type that restricts the underlying base type to the input element type requires one less type parameter.
1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15:
Tutorial contains a further explanation of this dependent types library.
API Reference contains automatically generated documentation for all types, modules, and functions in the library.
The DomainLib project is a sample library of useful dependent types:
trimmed, non-empty, non-null string
non-empty generic set
uppercase Latin string of undetermined or static length
digit string of undetermined or static length
integer restricted to a range
The DependentTypesConsole project runs demos on both the
'T1 -> 'T2and
'T -> 'Tstyle dependent types.
Several issues are available for discussion. Among the most interesting
The library is available under Public Domain license, which allows modification and redistribution for both commercial and non-commercial purposes. For more information see the License file in the GitHub repository.