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<'Cctor, 'Config, 'T, 'T2 when 'Cctor :> Cctor<'Config, 'T, 'T2>
                                            and  'Cctor : (new: unit -> 'Cctor)>

relies on a "constructor" type

1: 
type Cctor<'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 Cctor<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, Cctor 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.

Fork me on GitHub