DependentTypes

DependentTypes

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 ('T or 'T2). Extension methods are not yet supported.

The core dependent type

1: 
2: 

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

relies on a "constructor" type

1: 

type PiType<'Config, 'T, 'T2> (config: 'Config, vfn: 'Config -> 'T -> Option<'T2>)

which in turn requires a function 'Config -> 'T1 -> 'T2 option that validates the input element. Another type handles consuming the 'Config parameter.

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: 

open DependentTypes

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

    type DigitsValidator(config) = 
        inherit PiType<int, string, string>(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>
type Digits2 = DependentType<DigitsDef.ValidDigits2, int, string, string>
type Digits3 = DependentType<DigitsDef.ValidDigits3, int, string, string>
type Digits4 = DependentType<DigitsDef.ValidDigits4, int, string, string>

let digits = Digits.Create "093884765"
let digitsofLength3 = Digits3.Create "007"

Notes:

  1. The full validation function regExStringVerify is not shown.

  2. The presence of module DigitsDef is strictly for readability purposes, segregating the "helper" functions and types.

  3. All the helper types must have the same access level as the dependent type.
  4. Aliasing is optional, but obviously provides better readability.

  5. Yes, PiType is not really a constructor.

  6. With possible changes to the F# language, the intervening 'Config consuming helper type may be superfluous.

Alternate form of dependent types

Alternately, a dependent type that restricts the underlying base type to the input element type requires one less type parameter.

See the Tutorial and sample library of dependent types for an example of a generic collection type, Set<'T>.

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 

module NonEmptySetDef =
    let verifyNonEmptySet _ (value : Set<int>) =
        if value.Count > 0 then
            Some value  
        else
            None

    type NonEmptySetValidator() = 
        inherit Validator<unit, Set<int>>((), verifyNonEmptySet)

    type ValidNonEmptySet() = inherit NonEmptySetValidator()
    
type NonEmptyIntSet = LimitedValue<NonEmptySetDef.ValidNonEmptySet, unit, Set<int>>

let myNonEmptyIntSetOpt = [1;2;3] |> Set.ofList |> NonEmptyIntSet.TryCreate

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 static length

    digit string of undetermined or static length

    integer restricted to a range

  • The DependentTypesConsole project runs demos on both the 'T1 -> 'T2 and 'T -> 'T style dependent types.

  • Expecto test projects for both the DependentTypes library and the DomainLib sample dependent types.

Issues

Several issues are available for discussion. Among the most interesting

Contributing and copyright

This library is based on original experiments by @robkuz with the LimitedValue type, Creating Generic Wrappers for Validated Values. Further discussion 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<'PiType,'Config,'T,'T2 (requires default constructor)> =
type unit = Unit
module Option

from Microsoft.FSharp.Core
namespace DependentTypes
val verifyDigits : config:int -> value:string -> string option
Multiple items
type DigitsValidator =
  inherit PiType<int,string,string>
  new : config:int -> DigitsValidator

--------------------
new : config:int -> DigitsValidator
Multiple items
type PiType<'Config,'T,'T2> =
  new : config:'Config * vfn:('Config -> 'T -> Option<'T2>) -> PiType<'Config,'T,'T2>
  member TryCreate : x:'T -> Option<'T2>

--------------------
new : config:'Config * vfn:('Config -> 'T -> Option<'T2>) -> PiType<'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>
Multiple items
union case LimitedValue.DependentType: 'T -> LimitedValue<'Validator,'Config,'T>

--------------------
type DependentType<'PiType,'Config,'T,'T2 (requires 'PiType :> PiType<'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> -> Option<DependentType<'a,'b,'r,'s>> (requires 'x :> PiType<'y,'q,'r> and default constructor and 'a :> PiType<'b,'r,'s> and default constructor)
    static member Create : xs:'T list -> DependentType<'PiType,'Config,'T,'T2> list
    static member Create : xs:seq<'T> -> seq<DependentType<'PiType,'Config,'T,'T2>>
    static member Create : x:'T -> DependentType<'PiType,'Config,'T,'T2>
    static member Extract : x:DependentType<'PiType,'Config,'T,'T2> -> 'T2
    static member TryCreate : x:'T option -> Option<DependentType<'PiType,'Config,'T,'T2>>
    static member TryCreate : x:'T -> Option<DependentType<'PiType,'Config,'T,'T2>>
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>
Multiple items
type ValidDigits2 =
  inherit DigitsValidator
  new : unit -> ValidDigits2

--------------------
new : unit -> DigitsDef.ValidDigits2
type Digits3 = DependentType<DigitsDef.ValidDigits3,int,string,string>
Multiple items
type ValidDigits3 =
  inherit DigitsValidator
  new : unit -> ValidDigits3

--------------------
new : unit -> DigitsDef.ValidDigits3
type Digits4 = DependentType<DigitsDef.ValidDigits4,int,string,string>
Multiple items
type ValidDigits4 =
  inherit DigitsValidator
  new : unit -> ValidDigits4

--------------------
new : unit -> DigitsDef.ValidDigits4
val digits : DependentType<DigitsDef.ValidDigits,int,string,string>
static member DependentType.Create : xs:'T list -> DependentType<'PiType,'Config,'T,'T2> list
static member DependentType.Create : xs:seq<'T> -> seq<DependentType<'PiType,'Config,'T,'T2>>
static member DependentType.Create : x:'T -> DependentType<'PiType,'Config,'T,'T2>
val digitsofLength3 : DependentType<DigitsDef.ValidDigits3,int,string,string>
val verifyNonEmptySet : 'a -> value:Set<int> -> Set<int> option
val value : Set<int>
Multiple items
module Set

from Microsoft.FSharp.Collections

--------------------
type Set<'T (requires comparison)> =
  interface IComparable
  interface IEnumerable
  interface IEnumerable<'T>
  interface ICollection<'T>
  new : elements:seq<'T> -> Set<'T>
  member Add : value:'T -> Set<'T>
  member Contains : value:'T -> bool
  override Equals : obj -> bool
  member IsProperSubsetOf : otherSet:Set<'T> -> bool
  member IsProperSupersetOf : otherSet:Set<'T> -> bool
  ...

--------------------
new : elements:seq<'T> -> Set<'T>
property Set.Count: int
Multiple items
type NonEmptySetValidator =
  inherit Validator<unit,Set<int>>
  new : unit -> NonEmptySetValidator

--------------------
new : unit -> NonEmptySetValidator
Multiple items
type Validator<'Config,'T> =
  new : config:'Config * vfn:('Config -> 'T -> Option<'T>) -> Validator<'Config,'T>
  member Validate : x:'T -> Option<'T>

--------------------
new : config:'Config * vfn:('Config -> 'T -> Option<'T>) -> Validator<'Config,'T>
Multiple items
type ValidNonEmptySet =
  inherit NonEmptySetValidator
  new : unit -> ValidNonEmptySet

--------------------
new : unit -> ValidNonEmptySet
type NonEmptyIntSet = LimitedValue<NonEmptySetDef.ValidNonEmptySet,unit,Set<int>>
type LimitedValue<'Validator,'Config,'T (requires 'Validator :> Validator<'Config,'T> and default constructor)> =
  | DependentType of 'T
    member Value : 'T
    static member ConvertTo : x:LimitedValue<'x,'y,'q> -> Option<LimitedValue<'a,'b,'q>> (requires 'x :> Validator<'y,'q> and default constructor and 'a :> Validator<'b,'q> and default constructor)
    static member Create : xs:'T list -> LimitedValue<'Validator,'Config,'T> list
    static member Create : xs:seq<'T> -> seq<LimitedValue<'Validator,'Config,'T>>
    static member Create : x:'T -> LimitedValue<'Validator,'Config,'T>
    static member Extract : x:LimitedValue<'Validator,'Config,'T> -> 'T
    static member TryCreate : x:'T -> Option<LimitedValue<'Validator,'Config,'T>>
module NonEmptySetDef

from Index
Multiple items
type ValidNonEmptySet =
  inherit NonEmptySetValidator
  new : unit -> ValidNonEmptySet

--------------------
new : unit -> NonEmptySetDef.ValidNonEmptySet
val myNonEmptyIntSetOpt : Option<LimitedValue<NonEmptySetDef.ValidNonEmptySet,unit,Set<int>>>
val ofList : elements:'T list -> Set<'T> (requires comparison)
static member LimitedValue.TryCreate : x:'T -> Option<LimitedValue<'Validator,'Config,'T>>
F# Project
Fork me on GitHub