Dependent types tutorial

Trimmed, non-empty, non-null strings

This is an example of passing unit as the config. We will see later that passing a configuration other than unit, (), requires a second level of type inheritance.

Note that the module TrimNonEmptyStringDef helps format the code for readability. Otherwise it serves no functional purpose.

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

open DependentTypes
open DependentTypes.Helpers
open System

module TrimNonEmptyStringDef =
    let verifyTrimNonEmptyString _ (value : string) =
        if String.IsNullOrWhiteSpace value then
            None        
        else 
            Some <| value.Trim()

    type NonEmptyValidator() = 
        inherit Pi<unit, string, string option>((), verifyTrimNonEmptyString)

type TrimNonEmptyString = SomeDependentType<TrimNonEmptyStringDef.NonEmptyValidator, unit, string, string>

Generalized and specific type creation

Use the config input to make more specific types over a generalized validator function.

Construct the DependentType option one of three ways

mkDependentType function, requires type hint in let value
TryCreate for option base types this will lift option to the DependentType
Create is always safe (will not throw), but does not lift option to the DependentType

Note that passing a configuration other than unit, (), requires a second level of inheritance.

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

module RangeValidation =
    let validate normalize fn v =
        if fn (normalize v) then Some (normalize v) else None

    let validateRange (min,max) v = validate id (fun v -> v >= min && v <= max) v

    type NumRangeValidator(config) = inherit Pi<int * int, int, int option>(config, validateRange)

    type MaxPos100 () = inherit NumRangeValidator(0, 100)

type PositiveInt100 = SomeDependentType<RangeValidation.MaxPos100, int * int, int, int>

let a : PositiveInt100 = mkDependentType 100

let b = PositiveInt100.TryCreate 100

let c = PositiveInt100.Create 100

printfn "%A" c.Value

DependentType.Value returns the base type value.

TryCreate method

If the base type is an option type, and it was created with TryCreate, option is lifted to the DependentType itself. If the value is known to be Some, the unsafe function Helpers.someValue may be used to access the value.

If you have already returned the DependentType option Value, the Helper method flatten and forceValue will make your code less verbose.

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

let myGoodString = (TrimNonEmptyString.TryCreate "good string   ")

// SomeDependentType "good string"
printfn "%A" myGoodString

// "good string"
printfn "%s" <|
    match myGoodString with
    | Some goodString -> goodString.Value
    | None -> "this won't print"

// "good string"
printfn "%s" (flatten myGoodString)

let notTrimNonEmptyString = TrimNonEmptyString.TryCreate "    "

// true
printfn "%b" notTrimNonEmptyString.IsNone

Create method

For all 'T2 base types the Create method is safe (meaning it will not throw), but for option types if will not lift the option.

Here is an example of a dependent type with a simple 'T2 base type.

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

module UtcDateTimeDef =
    let verifyUtcDateTime _ (value : DateTime) =
        value.ToUniversalTime()     

    type UtcDateTimeValidator() = 
        inherit Pi<unit, DateTime, DateTime>((), verifyUtcDateTime)

    type ValidUtcDateTime () = inherit UtcDateTimeValidator()
    
type UtcDateTime = DependentType<UtcDateTimeDef.ValidUtcDateTime, unit, DateTime, DateTime> 

let utcTime = DateTime.Now |> UtcDateTime.Create

Base type of discriminated Union

Use F# discriminated union to mimic a type family of arbitrarily many members.

 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:

type IntegerOfSign =
        | PositiveInt of int
        | Zero of int
        | NegativeInt of int

module SumType =
    let intType _ (value : int) =
        match value with
        | v when v > 0 ->
            IntegerOfSign.PositiveInt v
        | v when v = 0 ->
            IntegerOfSign.Zero v
        | v ->
            IntegerOfSign.NegativeInt v

    type IntSumTypeDiscriminator() = 
        inherit Pi<unit, int, IntegerOfSign>((), intType)
    
type IntegerType = DependentType<SumType.IntSumTypeDiscriminator, unit, int, IntegerOfSign>

let s2 = IntegerType.Create -21
let s3 = IntegerType.Create 0
let s4 = IntegerType.Create 21

// DependentType (NegativeInt -21)
printfn "%A" s2

// DependentType (Zero 0)
printfn "%A" s3

// DependentType (PositiveInt 21)
printfn "%A" s4

Generic dependent types

You can also create generic dependent types.

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

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

    type NonEmptySetValidator<'T when 'T : comparison>() = 
        inherit Pi<unit, Set<'T>, Set<'T> option>((), verifyNonEmptySet)
  
type NonEmptySet<'T  when 'T : comparison> = SomeDependentType<NonEmptySetDef.NonEmptySetValidator<'T>, unit, Set<'T>, Set<'T>> 

let myNonEmptyIntSet = [1;2;3] |> Set.ofList |> NonEmptySet.Create
let myNonEmptyStringSet = ["Rob";"Jack";"Don"] |> Set.ofList |> NonEmptySet.Create

Limit values to ranges

Note that passing a configuration other than unit, (), requires a second level of inheritance.

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23:

module IntRange =
    let validate fn v =
        if fn v then Some v else None
    let validateRange (min,max) v = validate (fun v -> v >= min && v <= max) v
    let validateMin (min) v = validate (fun v -> v >= min) v
    let validateMax (max) v = validate (fun v -> v <= max) v

    type NumRangeValidator(config) = inherit Pi<int * int, int, int option>(config, validateRange)
    type MinNumRangeValidator(config) = inherit Pi<int, int, int option>(config, validateMin)
    type MaxNumRangeValidator(config) = inherit Pi<int, int, int option>(config, validateMax)

    type MaxPos100 () = inherit NumRangeValidator(0, 100)
    type MaxPos20000 () = inherit NumRangeValidator(0, 20000)
    type RangeMinus100To100 () = inherit NumRangeValidator(-100, 100)
    type Min101 () = inherit MinNumRangeValidator(101)
    type MaxMinus101 () = inherit MaxNumRangeValidator(-101)

type PositiveInt100' = SomeDependentType<IntRange.MaxPos100, int * int, int, int>
type PositiveInt20000 = SomeDependentType<IntRange.MaxPos20000, int * int, int, int>
type Minus100To100 = SomeDependentType<IntRange.RangeMinus100To100, int * int, int, int>

type GT100 = DependentType<IntRange.Min101, int, int, int option>
type LTminus100 = DependentType<IntRange.MaxMinus101, int, int, int option>

Working with the underlying element

Return the underlying typed element with the extract function or the Value property.

DependentType.ToString() implements the underlying 'T2 element's type ToString().

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

let a' = extract a
let b' = b.Value
let c' = c.Value

// Some 100
printfn "%A" a'

// "100"
printfn "%i" <| extract b'

// "100"
printfn "%i" c'

// Some 100
printfn "%A" <| a.ToString()

DependentPair

Useful for keeing the input element associated with the dependent type.

 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:

module SizeMax5Type =
    let validate normalize fn v =
        if fn (normalize v) then Some (normalize v) else None

    let validateLen len s = 
        validate id (fun (s:string) -> s.Length <= len) s

    type LenValidator(config) = 
        inherit Pi<int, string, string option>(config, validateLen)

    type PairLenValidator(config) = 
        inherit Sigma<int, string, string option>(config, validateLen)

    type SizeMax5 () = inherit LenValidator(5) 

    type SizeMax5Pair () = inherit PairLenValidator(5)

type StringMax5Pair = DependentPair<SizeMax5Type.SizeMax5Pair, int, string, string option>

let s100 = StringMax5Pair.Create "100"
let s100000 = StringMax5Pair.Create "100000"

// DependentPair ("100",Some "100")
printfn "%A" s100

// DependentPair ("100000",None)
printfn "%A" s100000

ConvertTo

If the output T2 base type of one depependent type is the input type T1 of another, you can convert elements directly from one type to another.

 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:

type IntegerNegNonNeg =
    | NonNegativeInt of int
    | NegativeInt of int

module NonNegativSumType =
    let intType _ (value : IntegerOfSign) =
        match value with
        | IntegerOfSign.PositiveInt v ->
            IntegerNegNonNeg.NonNegativeInt v
        | IntegerOfSign.Zero v ->
            IntegerNegNonNeg.NonNegativeInt v
        | IntegerOfSign.NegativeInt v ->
            IntegerNegNonNeg.NegativeInt v

    type IntSumTypeDiscriminator() = 
        inherit Pi<unit, IntegerOfSign, IntegerNegNonNeg>((), intType)
    
type IntegerSignType = DependentType<NonNegativSumType.IntSumTypeDiscriminator, unit, IntegerOfSign, IntegerNegNonNeg>

let s42 = IntegerType.Create 42
let s0  = IntegerType.Create 0
let s_42 = IntegerType.Create -42

// DependentType (PositiveInt 42)
printfn "%A" s42

// DependentType (Zero 0)
printfn "%A" s0

// DependentType (NegativeInt -42)
printfn "%A" s_42

let s42B : IntegerSignType = IntegerSignType.ConvertTo s42
let s0B :IntegerSignType = IntegerSignType.ConvertTo s0
let s_42B : IntegerSignType = convertTo s_42

// DependentType (NonNegativeInt 42)
printfn "%A" s42B

// DependentType (NonNegativeInt 0)
printfn "%A" s0B

// DependentType (NegativeInt -42)
printfn "%A" s_42B

Note: the type hints let s42B : IntegerSignType =, etc. are usually not necessary in compiled code when using the type's static method, but may be in FSI.

namespace DependentTypes

module Helpers

from DependentTypes

namespace System

val verifyTrimNonEmptyString : 'a -> value:string -> string option

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>

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

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

Multiple items
type NonEmptyValidator =
inherit Pi<unit,string,string option>
new : unit -> NonEmptyValidator

--------------------
new : unit -> NonEmptyValidator

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>

type unit = Unit

type 'T option = Option<'T>

type TrimNonEmptyString = SomeDependentType<TrimNonEmptyStringDef.NonEmptyValidator,unit,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

module TrimNonEmptyStringDef

from Tutorial

Multiple items
type NonEmptyValidator =
inherit Pi<unit,string,string option>
new : unit -> NonEmptyValidator

--------------------
new : unit -> TrimNonEmptyStringDef.NonEmptyValidator

val validate : normalize:('a -> 'b) -> fn:('b -> bool) -> v:'a -> 'b option

val normalize : ('a -> 'b)

val fn : ('b -> bool)

val v : 'a

val validateRange : min:'a * max:'a -> v:'a -> 'a option (requires comparison)

val min : 'a (requires comparison)

val max : 'a (requires comparison)

val v : 'a (requires comparison)

val id : x:'T -> 'T

Multiple items
type NumRangeValidator =
inherit Pi<(int * int),int,int option>
new : config:(int * int) -> NumRangeValidator

--------------------
new : config:(int * int) -> NumRangeValidator

val config : int * int

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

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

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

Multiple items
type MaxPos100 =
inherit NumRangeValidator
new : unit -> MaxPos100

--------------------
new : unit -> MaxPos100

type PositiveInt100 = SomeDependentType<RangeValidation.MaxPos100,(int * int),int,int>

module RangeValidation

from Tutorial

Multiple items
type MaxPos100 =
inherit NumRangeValidator
new : unit -> MaxPos100

--------------------
new : unit -> RangeValidation.MaxPos100

val a : PositiveInt100

val mkDependentType : x:'S -> 'T (requires member Create)

val b : SomeDependentType<RangeValidation.MaxPos100,(int * int),int,int> option

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

val c : SomeDependentType<RangeValidation.MaxPos100,(int * int),int,int>

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

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

property SomeDependentType.Value: int

val myGoodString : SomeDependentType<TrimNonEmptyStringDef.NonEmptyValidator,unit,string,string> option

val goodString : SomeDependentType<TrimNonEmptyStringDef.NonEmptyValidator,unit,string,string>

property SomeDependentType.Value: string

val flatten : x:'S -> 'U (requires member get_Value and member get_Value)

val notTrimNonEmptyString : SomeDependentType<TrimNonEmptyStringDef.NonEmptyValidator,unit,string,string> option

property Option.IsNone: bool

val verifyUtcDateTime : 'a -> value:DateTime -> DateTime

val value : DateTime

Multiple items
type DateTime =
  struct
    new : ticks:int64 -> DateTime + 10 overloads
    member Add : value:TimeSpan -> DateTime
    member AddDays : value:float -> DateTime
    member AddHours : value:float -> DateTime
    member AddMilliseconds : value:float -> DateTime
    member AddMinutes : value:float -> DateTime
    member AddMonths : months:int -> DateTime
    member AddSeconds : value:float -> DateTime
    member AddTicks : value:int64 -> DateTime
    member AddYears : value:int -> DateTime
    ...
  end

--------------------
DateTime ()
   (+0 other overloads)
DateTime(ticks: int64) : DateTime
   (+0 other overloads)
DateTime(ticks: int64, kind: DateTimeKind) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, calendar: Globalization.Calendar) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, hour: int, minute: int, second: int) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, hour: int, minute: int, second: int, kind: DateTimeKind) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, hour: int, minute: int, second: int, calendar: Globalization.Calendar) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, hour: int, minute: int, second: int, millisecond: int) : DateTime
   (+0 other overloads)
DateTime(year: int, month: int, day: int, hour: int, minute: int, second: int, millisecond: int, kind: DateTimeKind) : DateTime
   (+0 other overloads)

DateTime.ToUniversalTime() : DateTime

Multiple items
type UtcDateTimeValidator =
inherit Pi<unit,DateTime,DateTime>
new : unit -> UtcDateTimeValidator

--------------------
new : unit -> UtcDateTimeValidator

Multiple items
type ValidUtcDateTime =
inherit UtcDateTimeValidator
new : unit -> ValidUtcDateTime

--------------------
new : unit -> ValidUtcDateTime

type UtcDateTime = DependentType<UtcDateTimeDef.ValidUtcDateTime,unit,DateTime,DateTime>

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 UtcDateTimeDef

from Tutorial

Multiple items
type ValidUtcDateTime =
inherit UtcDateTimeValidator
new : unit -> ValidUtcDateTime

--------------------
new : unit -> UtcDateTimeDef.ValidUtcDateTime

val utcTime : DependentType<UtcDateTimeDef.ValidUtcDateTime,unit,DateTime,DateTime>

property DateTime.Now: DateTime

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

type IntegerOfSign =
  | PositiveInt of int
  | Zero of int
  | NegativeInt of int

union case IntegerOfSign.PositiveInt: int -> IntegerOfSign

union case IntegerOfSign.Zero: int -> IntegerOfSign

union case IntegerOfSign.NegativeInt: int -> IntegerOfSign

val intType : 'a -> value:int -> IntegerOfSign

val value : int

val v : int

Multiple items
type IntSumTypeDiscriminator =
inherit Pi<unit,int,IntegerOfSign>
new : unit -> IntSumTypeDiscriminator

--------------------
new : unit -> IntSumTypeDiscriminator

type IntegerType = DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

module SumType

from Tutorial

Multiple items
type IntSumTypeDiscriminator =
inherit Pi<unit,int,IntegerOfSign>
new : unit -> IntSumTypeDiscriminator

--------------------
new : unit -> SumType.IntSumTypeDiscriminator

val s2 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val s3 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val s4 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val verifyNonEmptySet : 'a -> value:Set<'T> -> Set<'T> option (requires comparison)

val value : Set<'T> (requires comparison)

Multiple items
module Set

from Microsoft.FSharp.Collections

--------------------
type Set<'T (requires comparison)> =
  interface IReadOnlyCollection<'T>
  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
  ...

--------------------
new : elements:seq<'T> -> Set<'T>

property Set.Count: int

Multiple items
type NonEmptySetValidator<'T (requires comparison)> =
inherit Pi<unit,Set<'T>,Set<'T> option>
new : unit -> NonEmptySetValidator<'T>

--------------------
new : unit -> NonEmptySetValidator<'T>

type NonEmptySet<'T (requires comparison)> = SomeDependentType<NonEmptySetDef.NonEmptySetValidator<'T>,unit,Set<'T>,Set<'T>>

module NonEmptySetDef

from Tutorial

val myNonEmptyIntSet : SomeDependentType<NonEmptySetDef.NonEmptySetValidator<int>,unit,Set<int>,Set<int>>

val ofList : elements:'T list -> Set<'T> (requires comparison)

val myNonEmptyStringSet : SomeDependentType<NonEmptySetDef.NonEmptySetValidator<string>,unit,Set<string>,Set<string>>

val validate : fn:('a -> bool) -> v:'a -> 'a option

val fn : ('a -> bool)

val validateMin : min:'a -> v:'a -> 'a option (requires comparison)

val validateMax : max:'a -> v:'a -> 'a option (requires comparison)

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

--------------------
new : config:int -> MinNumRangeValidator

val config : int

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

--------------------
new : config:int -> MaxNumRangeValidator

Multiple items
type MaxPos20000 =
inherit NumRangeValidator
new : unit -> MaxPos20000

--------------------
new : unit -> MaxPos20000

Multiple items
type RangeMinus100To100 =
inherit NumRangeValidator
new : unit -> RangeMinus100To100

--------------------
new : unit -> RangeMinus100To100

Multiple items
type Min101 =
inherit MinNumRangeValidator
new : unit -> Min101

--------------------
new : unit -> Min101

Multiple items
type MaxMinus101 =
inherit MaxNumRangeValidator
new : unit -> MaxMinus101

--------------------
new : unit -> MaxMinus101

type PositiveInt100' = SomeDependentType<IntRange.MaxPos100,(int * int),int,int>

module IntRange

from Tutorial

Multiple items
type MaxPos100 =
inherit NumRangeValidator
new : unit -> MaxPos100

--------------------
new : unit -> IntRange.MaxPos100

type PositiveInt20000 = SomeDependentType<IntRange.MaxPos20000,(int * int),int,int>

Multiple items
type MaxPos20000 =
inherit NumRangeValidator
new : unit -> MaxPos20000

--------------------
new : unit -> IntRange.MaxPos20000

type Minus100To100 = SomeDependentType<IntRange.RangeMinus100To100,(int * int),int,int>

Multiple items
type RangeMinus100To100 =
inherit NumRangeValidator
new : unit -> RangeMinus100To100

--------------------
new : unit -> IntRange.RangeMinus100To100

type GT100 = DependentType<IntRange.Min101,int,int,int option>

Multiple items
type Min101 =
inherit MinNumRangeValidator
new : unit -> Min101

--------------------
new : unit -> IntRange.Min101

type LTminus100 = DependentType<IntRange.MaxMinus101,int,int,int option>

Multiple items
type MaxMinus101 =
inherit MaxNumRangeValidator
new : unit -> MaxMinus101

--------------------
new : unit -> IntRange.MaxMinus101

val a' : int

val extract : x:'S -> 'T (requires member Extract)

val b' : SomeDependentType<RangeValidation.MaxPos100,(int * int),int,int>

property Option.Value: SomeDependentType<RangeValidation.MaxPos100,(int * int),int,int>

val c' : int

override SomeDependentType.ToString : unit -> string

val validateLen : len:int -> s:string -> string option

val len : int

val s : string

property String.Length: int

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

--------------------
new : config:int -> LenValidator

Multiple items
type PairLenValidator =
inherit Sigma<int,string,string option>
new : config:int -> PairLenValidator

--------------------
new : config:int -> PairLenValidator

Multiple items
type Sigma<'Config,'T,'T2> =
new : config:'Config * pi:('Config -> 'T -> 'T2) -> Sigma<'Config,'T,'T2>
member Create : x:'T -> 'T * 'T2

--------------------
new : config:'Config * pi:('Config -> 'T -> 'T2) -> Sigma<'Config,'T,'T2>

Multiple items
type SizeMax5 =
inherit LenValidator
new : unit -> SizeMax5

--------------------
new : unit -> SizeMax5

Multiple items
type SizeMax5Pair =
inherit PairLenValidator
new : unit -> SizeMax5Pair

--------------------
new : unit -> SizeMax5Pair

type StringMax5Pair = DependentPair<SizeMax5Type.SizeMax5Pair,int,string,string option>

Multiple items
union case DependentPair.DependentPair: 'T * 'T2 -> DependentPair<'Sigma,'Config,'T,'T2>

--------------------
type DependentPair<'Sigma,'Config,'T,'T2 (requires 'Sigma :> Sigma<'Config,'T,'T2> and default constructor)> =
  | DependentPair of 'T * 'T2
    member Value : 'T * 'T2
    static member Create : x:'T -> DependentPair<'Sigma,'Config,'T,'T2>

module SizeMax5Type

from Tutorial

Multiple items
type SizeMax5Pair =
inherit PairLenValidator
new : unit -> SizeMax5Pair

--------------------
new : unit -> SizeMax5Type.SizeMax5Pair

val s100 : DependentPair<SizeMax5Type.SizeMax5Pair,int,string,string option>

static member DependentPair.Create : x:'T -> DependentPair<'Sigma,'Config,'T,'T2>

val s100000 : DependentPair<SizeMax5Type.SizeMax5Pair,int,string,string option>

type IntegerNegNonNeg =
| NonNegativeInt of int
| NegativeInt of int

union case IntegerNegNonNeg.NonNegativeInt: int -> IntegerNegNonNeg

union case IntegerNegNonNeg.NegativeInt: int -> IntegerNegNonNeg

val intType : 'a -> value:IntegerOfSign -> IntegerNegNonNeg

val value : IntegerOfSign

Multiple items
type IntSumTypeDiscriminator =
inherit Pi<unit,IntegerOfSign,IntegerNegNonNeg>
new : unit -> IntSumTypeDiscriminator

--------------------
new : unit -> IntSumTypeDiscriminator

type IntegerSignType = DependentType<NonNegativSumType.IntSumTypeDiscriminator,unit,IntegerOfSign,IntegerNegNonNeg>

module NonNegativSumType

from Tutorial

Multiple items
type IntSumTypeDiscriminator =
inherit Pi<unit,IntegerOfSign,IntegerNegNonNeg>
new : unit -> IntSumTypeDiscriminator

--------------------
new : unit -> NonNegativSumType.IntSumTypeDiscriminator

val s42 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val s0 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val s_42 : DependentType<SumType.IntSumTypeDiscriminator,unit,int,IntegerOfSign>

val s42B : IntegerSignType

static member DependentType.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)

val s0B : IntegerSignType

val s_42B : IntegerSignType

val convertTo : x:'S -> 'T (requires member ConvertTo)