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:

type DependentType<'Pi, 'Config, 'T, 'T2 when 'Pi :> Pi<'Config, 'T, 'T2>  
                                         and  'Pi : (new: unit -> 'Pi)>

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:	`type Pi<'Config, 'T, 'T2> (config: 'Config, pi: 'Config -> 'T -> 'T2)`

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:

type SomeDependentType<'Pi, 'Config, 'T, 'T2 when 'Pi :> Pi<'Config, 'T, 'T2 option>  
                                             and  'Pi : (new: unit -> 'Pi)>

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:

open DependentTypes

module DigitsDef =
    let verifyDigits config value =
        regExStringVerify (new Regex("^[0-9]+$")) config value

    type DigitsValidator(config) = 
        inherit Pi<int, string, string option>(config, verifyDigits)

    type ValidDigits () = inherit DigitsValidator(0)
    type ValidDigits2 () = inherit DigitsValidator(2)
    type ValidDigits3 () = inherit DigitsValidator(3)
    type ValidDigits4 () = inherit DigitsValidator(4)
    
type Digits = DependentType<DigitsDef.ValidDigits, int, string, string option>
type Digits2 = DependentType<DigitsDef.ValidDigits2, int, string, string option>
type Digits3 = DependentType<DigitsDef.ValidDigits3, int, string, string option>
type Digits4 = DependentType<DigitsDef.ValidDigits4, int, string, string option>

type SomeDigits = SomeDependentType<DigitsDef.ValidDigits, int, string, string>
type SomeDigits2 = SomeDependentType<DigitsDef.ValidDigits2, int, string, string>
type SomeDigits3 = SomeDependentType<DigitsDef.ValidDigits3, int, string, string>
type SomeDigits4 = SomeDependentType<DigitsDef.ValidDigits4, int, string, string>

let digits = Digits.Create "093884765"
// DependentType (Some "093884765")

let digitsOfLength3 = Digits3.Create "007"
// DependentType (Some "007")

let notDigitsOfLength3 = Digits3.TryCreate "0007"
// None

printfn "%A" <| SomeDigits.TryCreate "093884765"
// Some (SomeDependentType "093884765")

printfn "%A" <| SomeDigits3.TryCreate "007"
// Some (SomeDependentType "007")

printfn "%A" <| SomeDigits3.TryCreate "0007"
// None

printfn "SomeDependentType Create is not safe: %A" <| SomeDigits3.Create "007"
// SomeDependentType Create is not safe: SomeDependentType "007"

printfn "System.NullReferenceException: %A" <| SomeDigits3.Create "0007"
// System.NullReferenceException: Object reference not set to an instance of an object.

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 the option of 'T2 to the DependentType.

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:

type DependentPair<'Sigma, 'Config, 'T, 'T2 when 'Sigma :> Sigma<'Config, 'T, 'T2>  
                                                 and 'Sigma : (new: unit -> 'Sigma)>

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:
1. trimmed, non-empty, non-null string
2. non-empty generic set
3. UTC datetime
4. uppercase Latin string of undetermined or specific length
5. digit string of undetermined or specific length
6. 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.

namespace System

namespace System.Text

namespace System.Text.RegularExpressions

val regExStringVerify : regex:Regex -> config:int -> value:string -> string option

val regex : Regex

Multiple items
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 config : int

val value : string

Multiple items
val string : value:'T -> string

--------------------
type string = String

Multiple items
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.IsNullOrWhiteSpace(value: string) : bool

union case Option.None: Option<'T>

val s' : string

String.Trim() : string
String.Trim([<ParamArray>] trimChars: char []) : string

Regex.IsMatch(input: string) : bool
Regex.IsMatch(input: string, startat: int) : bool

val length : str:string -> int

union case Option.Some: Value: 'T -> Option<'T>

type DependentType<'Pi,'Config,'T,'T2 (requires default constructor)> =

type unit = Unit

type 'T option = Option<'T>

namespace DependentTypes

val verifyDigits : config:int -> value:string -> string option

Multiple items
type DigitsValidator =
inherit Pi<int,string,string option>
new : config:int -> DigitsValidator

--------------------
new : config:int -> DigitsValidator

Multiple items
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>

Multiple items
val int : value:'T -> int (requires member op_Explicit)

--------------------
type int = int32

--------------------
type int<'Measure> = int

Multiple items
type ValidDigits =
inherit DigitsValidator
new : unit -> ValidDigits

--------------------
new : unit -> ValidDigits

Multiple items
type ValidDigits2 =
inherit DigitsValidator
new : unit -> ValidDigits2

--------------------
new : unit -> ValidDigits2

Multiple items
type ValidDigits3 =
inherit DigitsValidator
new : unit -> ValidDigits3

--------------------
new : unit -> ValidDigits3

Multiple items
type ValidDigits4 =
inherit DigitsValidator
new : unit -> ValidDigits4

--------------------
new : unit -> ValidDigits4

type Digits = DependentType<DigitsDef.ValidDigits,int,string,string option>

Multiple items
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

module DigitsDef

from Index

Multiple items
type ValidDigits =
inherit DigitsValidator
new : unit -> ValidDigits

--------------------
new : unit -> DigitsDef.ValidDigits

type Digits2 = DependentType<DigitsDef.ValidDigits2,int,string,string option>

Multiple items
type ValidDigits2 =
inherit DigitsValidator
new : unit -> ValidDigits2

--------------------
new : unit -> DigitsDef.ValidDigits2

type Digits3 = DependentType<DigitsDef.ValidDigits3,int,string,string option>

Multiple items
type ValidDigits3 =
inherit DigitsValidator
new : unit -> ValidDigits3

--------------------
new : unit -> DigitsDef.ValidDigits3

type Digits4 = DependentType<DigitsDef.ValidDigits4,int,string,string option>

Multiple items
type ValidDigits4 =
inherit DigitsValidator
new : unit -> ValidDigits4

--------------------
new : unit -> DigitsDef.ValidDigits4

type SomeDigits = SomeDependentType<DigitsDef.ValidDigits,int,string,string>

Multiple items
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

type SomeDigits2 = SomeDependentType<DigitsDef.ValidDigits2,int,string,string>

type SomeDigits3 = SomeDependentType<DigitsDef.ValidDigits3,int,string,string>

type SomeDigits4 = SomeDependentType<DigitsDef.ValidDigits4,int,string,string>

val digits : DependentType<DigitsDef.ValidDigits,int,string,string option>

static member DependentType.Create : x:'T -> DependentType<'Pi,'Config,'T,'T2>

val digitsOfLength3 : DependentType<DigitsDef.ValidDigits3,int,string,string option>

val notDigitsOfLength3 : DependentType<DigitsDef.ValidDigits3,int,string,string option> option

static member DependentType.TryCreate : x:Option<'T> -> DependentType<'Pi,'Config,'T,'T2> option
static member DependentType.TryCreate : x:'T -> DependentType<'Pi,'Config,'T,'T2> option

val printfn : format:Printf.TextWriterFormat<'T> -> 'T

static member SomeDependentType.TryCreate : x:'T -> SomeDependentType<'Pi,'Config,'T,'T2> option

static member SomeDependentType.Create : x:'T -> SomeDependentType<'Pi,'Config,'T,'T2>