[Discussion] Creating Generic Wrappers for Validated Values

[jackfoxy]

I'm very interested in this project, and probably have more feedback, but first I'm trying to get the "library" code building, and the LimitedValue type as printed does not build for me

type LimitedValue<'v, 'c, 't    when    'v :> Validator<'c, 't>
                                and     'v : (new: unit -> 'v)> = 
        LimitedValue of 't 
        with
            static member inline Create(x:'t) : Option<LimitedValue<'v, 'c, 't>> =
                x 
                |> (new 'v()).Validate 
                |>> LimitedValue

I'm not sure exactly what you have in mind here.

[jackfoxy]

I think I have it.

type LimitedValue<'v, 'c, 't    when    'v :> Validator<'c, 't>
                                and     'v : (new: unit -> 'v)> = 
        LimitedValue of 't 
        with
            static member inline Create(x:'t) : Option<LimitedValue<'v, 'c, 't>> =
                x 
                |> (new 'v()).Validate 
                |> Option.map LimitedValue

[jackfoxy]

I would like to have access to the underlying 't as a property named "Value", but I can't yet see how to get this to work

member __.Value : 't = ?

...it may not be so important.

[jackfoxy]

First of all, this is really excellent work. Some comments/suggestions:

1. This is a solution to dependent types. Maybe not a complete solution, but definitely a very wide ranging solution. As such, I encourage you to make that explicit. (Try changing then name LimitedValue to DependentType.)

2. The idea of a Create method only works (in my opinion) in limited circumstances. It must never throw, and it must return an instance of the type. When it returns type option, then the construction method should not be named Create, but rather TryParse. (That's the best name I have found.) Create is frequently misused.

3. All of the dependent types I have wanted to construct recently have come from the universe of strings. I think your solution is complete for these dependent types. One can retrieve the underlying 'T with ToString(), but what about other 'Ts? I do not see how to retrieve 'T generically. A Value property would work nicely, but I do not see how to implement it. (Perhaps you can see a solution.) I think this is crucial to important things like comparison, equality, map, etc.

namespace robkuz.DependentTypes

open System

type Validator<'Config, 'T> (config: 'Config, vfn: 'Config -> 'T -> Option<'T>) =
    member __.Validate(x:'T) : Option<'T> = vfn config x

type DependentType<'Validator, 'Config, 'T when 'Validator :> Validator<'Config, 'T>
                                           and  'Validator : (new: unit -> 'Validator)> =
    DependentType of 'T 
    
    with
        static member inline TryParse(x:'T) : Option<DependentType<'Validator, 'Config, 'T>> =
            x 
            |> (new 'Validator()).Validate 
            |> Option.map DependentType

Other Solutions

.NET IL cannot accept literals as type parameters. This is higher than an F# problem. Microsoft is understandably reticent to make changes to IL (they have the highest standards for backwards compatibility), especially with .NET Core going on now. I think IL is open-sourced somewhere. Maybe if someone demonstrates a change to accept integers and arrays as type parameters Microsoft may consider accepting the change, someday.

The other thing I have thought about is a generative type provider. I believe it will accept literals, but up until now TPs do not accept other types. I have heard of people trying to solve this problem.

[robkuz]

Hey Jack,

thanks for your comments.

1. I wouldn't mind calling this concept "Dependent Type" but then ... Isn't that a bit to boasting?
2. TryParse is certainly a good name if we are handling with strings, however this should really work with a lot of other basic types it works even with composite types as shown with the example of the VATValidator. So I think parse is somehow not to correct name. What if we rename it TryMake or TryCreate?
3. I have choosen extract for your use case. The reason being mainly that within our own codebase we are using Fsharpplus and there is a Comonad for that. Now I don't mind to add an additional .Value property and given that Allow _.Property shorthand for accessor functions fsharp/fslang-suggestions#506 will be implemented maybe sometime soon it will also lend itself for composition.

Other Solutions)
I didn't know that IL dependency - however I am not suprised ;-)
Nevertheless I think it should be possible if the F# compiler would generate that classes on the fly

lets say we have this

type SomeGeneric<'a,'b> = {a: 'a; b: 'b}
type FixedValues = SomeGeneric<100, "foo">

This could be easily expanded into

type SomeGeneric<'a,'b> = {a: 'a; b: 'b}

type Validator_FixedValues_100() = inherit Validator<int, int>(100, validateSingletonValue)
type Validator_FixedValues_foo() = inherit Validator<string, string>("foo", validateSingletonValue)
type Value_100()= LimitedValue<Validator_FixedValues_100, int, int>
type Value_foo()= LimitedValue<Validator_FixedValues_foo, string, string>

type FixedValues = SomeGeneric<Value_100, Value_foo>

on the fly

[jackfoxy]

I'm having fun playing with this.

1. It is not boasting when this solution addresses a wide range of dependent type functionality. I even created a demo dependent function (see below). The only thing missing would be creating dependent types with underlying type 'T2 from 'T. That would probably require a type signature of <'Validator, 'Config, 'T, 'Cctor<'T, 'T2>>, and as you point out, your solution is already complex enough (but still very usable). So I'm not advocating this extension, just pointing out how close you are to covering the entire theoretical case. Of the dependent type covering languages https://en.wikipedia.org/wiki/Dependent_type#Comparison_of_languages_with_dependent_types I am not aware of many of these being widely used in common production software development. Does Idris do a better job of covering dependent types in a less complex manner?

2. I did a little more research, and you are clearly in the majority opinion of restricting the meaning of the verb parse to operating only on text. I have taken a broader view for a long time because there is no good word for the other cases. So TryCreate is fine (but I still prefer TryParse).

3. I'm embarrassed. I jumped right into investigating your system without finishing the article! I completely overlooked extract and convertTo. The only annoyance I have found is as a static member, convertTo still requires a type hint. I'm pretty certain this is a limitation of F# unification and not anything that can be addressed immediately (but maybe as part of the language suggestion).

let d : Option<PositiveInt20000> = PositiveInt20000.ConvertTo c

If it did not require the hint I would advocate for the static member to be an overload of the TryParse (TryCreate) static member.

Language suggestion and/or NuGet package

I hope others contribute comments soon. I think some more perspectives would be valuable before submitting a language suggestion and/or creating a NuGet package. I like your idea for using this to leverage static type parameters, but I haven't experimented with that yet.

Not including static parameters (which should just work in the language suggestion, and I haven't thought about it for a package) this is my current take on structuring the namespace.

namespace robkuz.DependentTypes

module DependentTypes =
    let inline mkLimitedValue (x: ^S) : Option< ^T> = 
        (^T: (static member TryParse: ^S -> Option< ^T>) x)

    let inline extract (x:^S) = 
        (^S: (static member Extract: ^S -> ^T) x)

    let inline convertTo (x: ^S) : Option< ^T> = 
        (^T: (static member ConvertTo: ^S -> Option< ^T>) x)

open DependentTypes
open System

type Validator<'Config, 'T> (config: 'Config, vfn: 'Config -> 'T -> Option<'T>) =
    member __.Validate(x:'T) : Option<'T> = vfn config x

type DependentType<'Validator, 'Config, 'T when 'Validator :> Validator<'Config, 'T>
                                           and  'Validator : (new: unit -> 'Validator)> =
    DependentType of 'T 
    
    with
        member __.Value = 
            let (DependentType s) = __
            s
        static member Extract (x : DependentType<'Validator, 'Config, 'T> ) = 
            let (DependentType s) = x
            s
        static member TryParse(x:'T) : Option<DependentType<'Validator, 'Config, 'T>> =
            (new 'Validator()).Validate x
            |> Option.map DependentType

        static member inline ConvertTo(x : DependentType<'x, 'y, 'q> ) : Option<DependentType<'a, 'b, 'q>> = 
            let (DependentType v) = x
            mkLimitedValue v

Dependent Function

As promised a dependent function.

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

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

type RangeMinus100To100 () = inherit NumRangeValidator(-100, 100)
type Min101 () = inherit MinNumRangeValidator(101)
type MaxMinus101 () = inherit MaxNumRangeValidator(-101)
type Minus100To100 = DependentType<RangeMinus100To100, int * int, int>

type GT100 = DependentType<Min101, int, int>
type LTminus100 = DependentType<MaxMinus101, int, int>

/// this is a dependent function
/// the type hint is not necessary, only to enhance the intellisense
let f n : DependentType<_, _, int> =
    match n with
    | n' when n' < -100 -> (LTminus100.TryParse n).Value |> box
    | n' when n' > 100 -> (GT100.TryParse n).Value |> box
    | _ -> (Minus100To100.TryParse n ).Value|> box
    |> unbox

let lTminus100 : LTminus100 = f -200
let gT100 : GT100 = f 101
let minus100To100 : Minus100To100 = f 1

[jackfoxy]

Link to article https://robkuz.github.io/Limited-Values/

[robkuz]

Hey Jack,

1. Maybe it's not boasting maybe it is. I must admit my dependent type foo isn't particular strong. I toyed around with Idris and read a bit about it. But really I have only a very coarse grained grasp of it. Certainly not on the theoretical level. The only thing I can say is that I somehow assumed (?) that DTs are working at compile time. E.g. it wouldn't be possible let a : GT100 = mkLimitedValue -1 to compile in a real DTL?
   Where as my proposed solution does the checking at runtime (sadly so) as the usage of Option is testament to. Am I wrong in this view?

As for your suggestion

The only thing missing would be creating dependent types with underlying type 'T2 from 'T.
That would probably require a type signature of <'Validator, 'Config, 'T, 'Cctor<'T, 'T2>>,

What can I do with this? Can you give some code examples?

Another point is that 'Cctor<'T, 'T2> would be a higher kinded. Which we can't express atm.
We can encode it but this will make the solution more complex. But then ... maybe there is a good reason to do so.

[jackfoxy]

Rob,
I think you are right that languages claiming dependent types resolve the types at compile time. On the other hand, most useful software has to deal with external data that is weakly typed. Deciding if it belongs to a stronger type is what LimitedValue does on an element by element basis, the type theoretical definition of dependent type. And how can you decide regarding external data at compile time?

I'm not familiar with Idris either, and now I'm trying to wrap my head around the utility of resolving dependent types at compile time. I think language professionals and enthusiasts think of dependent types more in solving formal methods problems, than solving day-to-day business problems.

So my view is going to be controversial.

I realize I'm misusing Cctor. I couldn't think of a better name.

Anyway, I think your LimitedValue<'T> alone is by far the most useful and common case. I put forward the idea of <'T, 'T2> only for completeness of the theoretical dependent type. I can only make some contrived examples (see below).

Also I want to point out my previous "dependent function" example is completely contrived. I can't think of a way it could be useful in any strongly typed language.

My first guess at implementing <'T, 'T2> was too complicated. Contemplating your original work on LimitedValue I realized it only takes minor modifications to make it work as <'T, 'T2>.

(To keep this issue thread readable I'm posting 2 more comments.)

[jackfoxy]

Modifications to LimitedValue to achieve a dependent type that takes 'T to 'T2.

namespace robkuz.DependentTypes2

module DependentTypes2 =
    let inline mkDependentType (x: ^S) : Option< ^T> = 
        (^T: (static member TryParse: ^S -> Option< ^T>) x)

    let inline extract (x:^S) = 
        (^S: (static member Extract: ^S -> ^T) x)

    let inline convertTo (x: ^S) : Option< ^T> = 
        (^T: (static member ConvertTo: ^S -> Option< ^T>) x)

open DependentTypes2
open System

type Cctor<'Config, 'T, 'T2> (config: 'Config, vfn: 'Config -> 'T -> Option<'T2>) =
    member __.TryCreate(x:'T) : Option<'T2> = vfn config x

type DependentType<'Cctor, 'Config, 'T, 'T2 when 'Cctor :> Cctor<'Config, 'T, 'T2>
                                            and  'Cctor : (new: unit -> 'Cctor)> =
    DependentType of 'T2 
    
    with
        member __.Value = 
            let (DependentType s) = __
            s
        static member Extract (x : DependentType<'Cctor, 'Config, 'T, 'T2> ) = 
            let (DependentType s) = x
            s
        static member TryParse(x:'T) : Option<DependentType<'Cctor, 'Config, 'T, 'T2>> =
            (new 'Cctor()).TryCreate x
            |> Option.map DependentType

        static member inline ConvertTo(x : DependentType<'x, 'y, 'q, 'r> ) : Option<DependentType<'a, 'b, 'r, 's>> = 
            let (DependentType v) = x
            mkDependentType v     

[jackfoxy]

Examples of dependent types taking 'T to 'T2.

Perhaps my examples are not too contrived, and someone else could think of this being useful.

(* 'T -> 'T2 tests existing LimitValue tests where 'T = 'T2 *)

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 Cctor<int, string, string>(config, validateLen)

type Size5 () = inherit LenValidator(5) 

type String5 = DependentType<Size5, int, string, string>
let okString = String5.TryParse "short" // Some
let failString = String5.TryParse "much too long" //None

let z = okString.Value
printfn "%s" z.Value

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

type NumRangeValidator(config) = inherit Cctor<int * int, int, int>(config, validateRange)
type MinNumRangeValidator(config) = inherit Cctor<int, int, int>(config, validateMin)
type MaxNumRangeValidator(config) = inherit Cctor<int, int, int>(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 = DependentType<MaxPos100, int * int, int, int>
type PositiveInt20000 = DependentType<MaxPos20000, int * int, int, int>
type Minus100To100 = DependentType<RangeMinus100To100, int * int, int, int>

type GT100 = DependentType<Min101, int, int, int>
type LTminus100 = DependentType<MaxMinus101, int, int, int>

let a: Option<PositiveInt100> = mkDependentType 100
let b = a.Value |> extract
let c = a.Value
let c' : Option<PositiveInt20000> = convertTo c
let d : Option<PositiveInt20000> = PositiveInt20000.ConvertTo c

printfn "%i" d.Value.Value

/// this is a dependent function
/// the type hint is not necessary, only to enhance the intellisense
let f n : DependentType<_, _, int, int> =
    match n with
    | n' when n' < -100 -> (LTminus100.TryParse n).Value |> box
    | n' when n' > 100 -> (GT100.TryParse n).Value |> box
    | _ -> (Minus100To100.TryParse n ).Value|> box
    |> unbox

let lTminus100 : LTminus100 = f -200
let gT100 : GT100 = f 101
let minus100To100 : Minus100To100 = f 1

(* 'T -> 'T2 test 1*)

let tryConstruct normalize fn v =
    fn (normalize v)

let tryConstructIndexToString i = 
    tryConstruct id (fun i' -> 
        (match i' with
        | n when n < 0 -> "negative"
        | n when n > 0 -> "positive"
        | _ -> "zero" )
        |> Some ) i

let tryIndexToString _ v = tryConstruct id tryConstructIndexToString v

type IndexToStringCctor() = 
    inherit Cctor<unit, int, string>((), tryIndexToString)

type IndexToString = DependentType<IndexToStringCctor, unit, int, string>

let neg =  (IndexToString.TryParse -100).Value

printfn "%s" neg.Value

let zero : Option<IndexToString> = mkDependentType 0
let zeroExtracted  = zero.Value |> extract
let zeroVal = zero.Value
let zeroValToString5 : Option<String5> = convertTo zeroVal

(* 'T -> 'T2 test 2*)

let tryConstructMultiplyToString multiplier i = 
    tryConstruct id (fun i' -> 
        (multiplier * i').ToString()
        |> Some ) i

type Multiply5StringCctor() = 
    inherit Cctor<int, int, string>(5, tryConstructMultiplyToString)

type Multiply5String = DependentType<Multiply5StringCctor, int, int, string>

let neg500 =  (Multiply5String.TryParse -100).Value

printfn "%s" neg500.Value

let neg500' : Option<Multiply5String> = mkDependentType -100
let neg500Extracted  = neg500'.Value |> extract
let neg500Val = neg500'.Value
let neg500ValToString5 : Option<String5> = convertTo neg500Val

[robkuz]

Hey Jack,

thanks for the further input.
If I understand that correctly you are proposing a merging of validation code with type transformation code.
I must admit my gut feeling would be not to do that as it "seems" (purely subjectively) that this stacks to
much stuff into one single "concept". But then there is also counter arguments

• You already implemented it and that one additional generic parameter isn't so bad at all
• My own implementation did "cheat" on that already. At least for strings i am normalizing the input which in a way is a type transformation already

Nevertheless my preference would be to do this type transformation via some map. Something like

let a: Max10Int = (tryMake 9).Value
let b: Len2String = map (fun x -> sprintf "%i" x) a

While I was pondering about this I became painfully aware about some serious downsides of the actual implementation.
Even thou this little type DependentType (LimitedValue) looks pretty much like a functor. It is not.

A functor needs to be structure preserving so a potential map function would look like this

let map f (v:DependentType<'a,'b,'c,'d>) : DependentType<'w,'x,'y,'z> =
    let (DependentType v') = v
    let r = v' |> f |> DependentType
    match r with
    | Some x -> r  //we can not return an Option here but must return a DependentType
    | _ -> failwith "OOOO!"

and then we can easily see this happen

let a: Max10Int = (tryMake 9).Value
let b: Max10Int = map (fun x -> x + 2) a

Bummer!

So I think the only way to allow for a proper map (and also bind) would be to redesign the type.
Here is an attempt

module DependentTypes2Fns =
    let inline tryMake (x: ^S) : ^T = 
        (^T: (static member TryMake: ^S -> ^T) x)

    let inline extract (x:^S) = 
        (^S: (static member Extract: ^S -> ^T) x)

    let inline convertTo (x: ^S) : Option< ^T> = 
        (^T: (static member ConvertTo: ^S -> Option< ^T>) x)

    let inline map f (x: ^S) : ^T = 
        (^S: (static member Map: ^S -> ^Q -> ^T) (x, f))

module DependentTypes2 =
    open DependentTypes2Fns
    type Validator<'Config, 'T> (config: 'Config, vfn: 'Config -> 'T -> Option<'T>) =
        member __.TryMake(x:'T) : Option<'T> = vfn config x
    
    type DependentType<'Validator, 'Config, 'T when 'Validator :> Validator<'Config, 'T>
                                                and  'Validator : (new: unit -> 'Validator)> =
        | DependentType of 'T
        | Failure of string 
        
        with
            member this.Value =
                match this with
                | DependentType v -> v
                | _ -> failwith "This is a Failure"
            static member TryMake(x:'T) : DependentType<'Validator, 'Config, 'T> =
                match (new 'Validator()).TryMake x with
                | Some v    -> DependentType v
                | _         -> Failure (sprintf "can not create this type %A" (typeof<DependentType<'Validator, 'Config, 'T>>)) 
            static member Extract (x : DependentType<'Validator, 'Config, 'T> ) = x.Value
            static member inline Map (x : DependentType<'a, 'b, 'c> , f : 'c -> 'q) : DependentType<'o, 'p, 'q> =
                match x with
                | DependentType v -> v |> f |> tryMake
                | Failure v -> Failure v
            static member inline ConvertTo(x : DependentType<'a, 'b, 'c> ) : DependentType<'o, 'p, 'q> = map id x
                
    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 Validator<int, string>(config, validateLen)
    
    type Size5 () = inherit LenValidator(5) 
    
    type String5 = DependentType<Size5, int, string>
    let okString = String5.TryMake "cool" // DependentType
    let failString = String5.TryMake "much too long" //Failure

    let addExclamation x = sprintf "%A!" x    
    let a: String5 = map addExclamation okString // DependentType<_,_, "cool!">
    let b: String5 = a |>> addExclamation        // Failure

[jackfoxy]

Hey Rob,

Failure is not an option. I hope you like my pun ;)

In seriousness, as you noted, LimitedValue/DependentType is not a functor. Maybe TryMap and TryBind static members have merit, but I don't think they are necessary to the core type.

I may have taken this thread off on too many tangents. I wanted to investigate corner and edge cases. I still want to apply this to a real library of mine (and I have one in mind) to reinforce my opinions, but as of now my thinking is:

1. Whatever it is called, the <'T> type with member Value and static members TryCreate, Extract, ConvertTo, and public inline methods is the core functionality. The language suggestion should probably be limited to this.

2. The language suggestion should include your literal type parameter solution.

3. I think it makes sense to create a demonstration library project with Nuget package, tests, and github.io docs/tutorial before submitting a language suggestion. I'd be willing to do most of this work, but you should publish it. Obviously the literal type solution cannot be part of the package.

4. I prefer the name DependentType, and think this gives F# some "bragging rights", but I also realize this is controversial, and if too controversial it would be counter-productive. You and Don should have final say on this.

5. I also prefer TryParse, but realize my broad definition of parse is a minority view and I don't want it to get in the way of success.

[jackfoxy]

Hi Rob,

I had a very good experience converting some types in a real library to dependent types and then using those types productively.

• trimmed, non-empty, non-null string

• non-empty integer set

• utc datetime

• uppercase Latin string of undetermined or static length

• digit string of undetermined or static length

Some lessons learned:

In my cases I would like some more create overload methods. TryCreate/TryParse would suffice if users could add their own extension methods, however this does not seem possible. So I think all the useful overloads need to be part of the base library. This is a little messy, but there is precedent in the .NET Framework of some classes with many overloads. Extension methods would also let users be creative in other ways. Of course there are other ways for users to handle these cases by creating their own functions over TryCreate/TryParse.

Added ToString() to support the uderlying type's ToString().

Dependent Types apparently preserve the equality and comparison behavior of the underlying type. (very nice)

I could not find a way to use this technique for generic dependent types, e.g. NonEmptySet<'T>. (This does not matter much. I'm just remarking that this is so.)