DependentTypes
In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type...
from Wikipedia article, Dependent type
This project is an experiment in bringing dependent types to F# for supporting finer levels of type granularity in a consistent manner.
Dependent types in logic and computer science take an element of a specific type and output a typed element in a family of types. F# does not support a family of types in a
generic sense, but we can still use F# and .NET types as output types that have family-like characteristics. This library presents generic dependent types, taking an element
of a specific input type to a new base type through a typed function 'T1 -> 'T2
.
The base 'T2
output types can be:
- any F# or .NET type, a family of one type
- an F# option type, the input element does or does not belong to the output underlying type, mimicking a family of two types
- an F# discriminated union type, the input element belongs to some member of the DU, mimicking a family of arbitrarily many types
The dependent type
1: 2: |
|
has a type parameter that includes a configuration, and a typed pi function, which maps input elements of the specified type to elements of the output type.
1:
|
|
The configuration is a convenience allowing re-use of the same function code to serve multiple dependent types by passing any desired parameters.
The most convenient type implementation for pi functions emitting an option type is SomeDependentType
.
1: 2: |
|
The construction of similar dependent types sharing the same pi function 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: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 39: 40: 41: 42: 43: 44: 45: 46: 47: |
|
Notes:
The full validation function
regExStringVerify
is not shown. A config value < 1 accepts digit strings of any length.The presence of
module DigitsDef
is 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 for providing better readability.
TryCreate
lifts theoption
of'T2
to theDependentType
.
Dependent types support the same equality and comparison traits as their base 'T2
type.
Extension methods are not yet supported.
DependentPairs
The dependent pair
1: 2: |
|
is a pair of the input element and resulting dependent type. Usage is similar to that of dependent types.
Samples & documentation
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
- UTC datetime
- uppercase Latin string of undetermined or specific length
- digit string of undetermined or specific length
- integer restricted to a range
The DependentTypesConsole project runs demos of dependent types.
Expecto test projects for both the DependentTypes library and the DomainLib sample dependent types.
Contributing and copyright
This library is based on original experiments by @robkuz with the LimitedValue type: Creating Generic Wrappers for Validated Values. Further discussion can be found here.
You can report issues, fork the project, and submit pull requests. Please also add tests and samples that can be turned into documentation.
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.
type Regex =
new : pattern:string -> Regex + 2 overloads
member GetGroupNames : unit -> string[]
member GetGroupNumbers : unit -> int[]
member GroupNameFromNumber : i:int -> string
member GroupNumberFromName : name:string -> int
member IsMatch : input:string -> bool + 1 overload
member Match : input:string -> Match + 2 overloads
member MatchTimeout : TimeSpan
member Matches : input:string -> MatchCollection + 1 overload
member Options : RegexOptions
...
--------------------
Regex(pattern: string) : Regex
Regex(pattern: string, options: RegexOptions) : Regex
Regex(pattern: string, options: RegexOptions, matchTimeout: TimeSpan) : Regex
val string : value:'T -> string
--------------------
type string = String
type String =
new : value:char -> string + 7 overloads
member Chars : int -> char
member Clone : unit -> obj
member CompareTo : value:obj -> int + 1 overload
member Contains : value:string -> bool
member CopyTo : sourceIndex:int * destination:char[] * destinationIndex:int * count:int -> unit
member EndsWith : value:string -> bool + 2 overloads
member Equals : obj:obj -> bool + 2 overloads
member GetEnumerator : unit -> CharEnumerator
member GetHashCode : unit -> int
...
--------------------
String(value: nativeptr<char>) : String
String(value: nativeptr<sbyte>) : String
String(value: char []) : String
String(c: char, count: int) : String
String(value: nativeptr<char>, startIndex: int, length: int) : String
String(value: nativeptr<sbyte>, startIndex: int, length: int) : String
String(value: char [], startIndex: int, length: int) : String
String(value: nativeptr<sbyte>, startIndex: int, length: int, enc: Text.Encoding) : String
String.Trim([<ParamArray>] trimChars: char []) : string
Regex.IsMatch(input: string, startat: int) : bool
type DigitsValidator =
inherit Pi<int,string,string option>
new : config:int -> DigitsValidator
--------------------
new : config:int -> DigitsValidator
type Pi<'Config,'T,'T2> =
new : config:'Config * pi:('Config -> 'T -> 'T2) -> Pi<'Config,'T,'T2>
member Create : x:'T -> 'T2
--------------------
new : config:'Config * pi:('Config -> 'T -> 'T2) -> Pi<'Config,'T,'T2>
val int : value:'T -> int (requires member op_Explicit)
--------------------
type int = int32
--------------------
type int<'Measure> = int
type ValidDigits =
inherit DigitsValidator
new : unit -> ValidDigits
--------------------
new : unit -> ValidDigits
type ValidDigits2 =
inherit DigitsValidator
new : unit -> ValidDigits2
--------------------
new : unit -> ValidDigits2
type ValidDigits3 =
inherit DigitsValidator
new : unit -> ValidDigits3
--------------------
new : unit -> ValidDigits3
type ValidDigits4 =
inherit DigitsValidator
new : unit -> ValidDigits4
--------------------
new : unit -> ValidDigits4
union case DependentType.DependentType: 'T2 -> DependentType<'Pi,'Config,'T,'T2>
--------------------
type DependentType<'Pi,'Config,'T,'T2 (requires 'Pi :> Pi<'Config,'T,'T2> and default constructor)> =
| DependentType of 'T2
override ToString : unit -> string
member Value : 'T2
static member ConvertTo : x:DependentType<'x,'y,'q,'r> -> DependentType<'a,'b,'r,'s> (requires 'x :> Pi<'y,'q,'r> and default constructor and 'a :> Pi<'b,'r,'s> and default constructor)
static member Create : x:'T -> DependentType<'Pi,'Config,'T,'T2>
static member Extract : x:DependentType<'Pi,'Config,'T,'T2> -> 'T2
static member TryCreate : x:Option<'T> -> DependentType<'Pi,'Config,'T,'T2> option
static member TryCreate : x:'T -> DependentType<'Pi,'Config,'T,'T2> option
from Index
type ValidDigits =
inherit DigitsValidator
new : unit -> ValidDigits
--------------------
new : unit -> DigitsDef.ValidDigits
type ValidDigits2 =
inherit DigitsValidator
new : unit -> ValidDigits2
--------------------
new : unit -> DigitsDef.ValidDigits2
type ValidDigits3 =
inherit DigitsValidator
new : unit -> ValidDigits3
--------------------
new : unit -> DigitsDef.ValidDigits3
type ValidDigits4 =
inherit DigitsValidator
new : unit -> ValidDigits4
--------------------
new : unit -> DigitsDef.ValidDigits4
union case SomeDependentType.SomeDependentType: 'T2 -> SomeDependentType<'Pi,'Config,'T,'T2>
--------------------
type SomeDependentType<'Pi,'Config,'T,'T2 (requires 'Pi :> Pi<'Config,'T,'T2 option> and default constructor)> =
| SomeDependentType of 'T2
override ToString : unit -> string
member Value : 'T2
static member ConvertTo : x:SomeDependentType<'x,'y,'q,'r> -> SomeDependentType<'a,'b,'r,'s> (requires 'x :> Pi<'y,'q,'r option> and default constructor and 'a :> Pi<'b,'r,'s option> and default constructor)
static member Create : x:'T -> SomeDependentType<'Pi,'Config,'T,'T2>
static member Extract : x:SomeDependentType<'Pi,'Config,'T,'T2> -> 'T2
static member TryCreate : x:'T -> SomeDependentType<'Pi,'Config,'T,'T2> option
static member DependentType.TryCreate : x:'T -> DependentType<'Pi,'Config,'T,'T2> option