Skip to content
This repository has been archived by the owner on Apr 18, 2020. It is now read-only.

Starting to verify laws #4

Merged
merged 9 commits into from
Jan 2, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
11 changes: 11 additions & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
sudo: false
language: csharp
dist: trusty
dotnet: 2.0.0
script:
- dotnet restore
- dotnet build
- dotnet test test/Tests
branches:
only:
- master
16 changes: 16 additions & 0 deletions appveyor.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@

version: 1.0.{build}
configuration: Release
before_build:
- dotnet restore
build_script:
- dotnet build
test_script:
- dotnet test test/Tests
nuget:
account_feed: false
project_feed: false
disable_publish_on_pr: true
branches:
only:
- master
110 changes: 49 additions & 61 deletions src/Validations/Library.fs
Original file line number Diff line number Diff line change
Expand Up @@ -4,114 +4,102 @@ open FSharpPlus
open FSharpPlus.Lens
open FSharpPlus.Compatibility.Haskell

/// | An @AccValidation@ is either a value of the type @err@ or @a@, similar to 'Either'. However,
/// the 'Applicative' instance for @AccValidation@ /accumulates/ errors using a 'Semigroup' on @err@.
/// In contrast, the @Applicative@ for @Either@ returns only the first error.
/// An 'AccValidation' is either a value of the type 'err or 'a, similar to 'Either'. However,
/// the 'Applicative' instance for 'AccValidation' /accumulates/ errors using a 'Semigroup' on 'err.
/// In contrast, the Applicative for 'Either returns only the first error.
///
/// A consequence of this is that @AccValidation@ has no 'Data.Functor.Bind.Bind' or 'Control.Monad.Monad' instance. This is because
/// such an instance would violate the law that a Monad's 'Control.Monad.ap' must equal the
/// @Applicative@'s 'Control.Applicative.<*>'
/// A consequence of this is that 'AccValidation' is not a monad. There is no f#+ 'Bind' method since
/// that would violate monad rules.
///
/// An example of typical usage can be found <https://github.com/qfpl/validation/blob/master/examples/src/Email.hs here>.
///
//[<StructuralEquality>]
//[<StructuralComparison>]
type AccValidation<'err,'a> =
| AccFailure of 'err
| AccSuccess of 'a

module AccValidation=
let inline map (f:'T->'U) x=
match x with
| AccFailure e -> AccFailure e
| AccSuccess a -> AccSuccess (f a)
let inline map (f:'T->'U)=function
|AccFailure e -> AccFailure e
|AccSuccess a -> AccSuccess (f a)
let inline apply e1' e2' =
match e1',e2' with
| AccFailure e1, AccFailure e2 -> AccFailure (plus e1 e2)
| AccFailure e1, AccSuccess _ -> AccFailure e1
| AccSuccess _, AccFailure e2 -> AccFailure e2
| AccSuccess f, AccSuccess a -> AccSuccess (f a)
|AccFailure e1, AccFailure e2 -> AccFailure (plus e1 e2)
|AccFailure e1, AccSuccess _ -> AccFailure e1
|AccSuccess _, AccFailure e2 -> AccFailure e2
|AccSuccess f, AccSuccess a -> AccSuccess (f a)
let inline foldr f x = function
| (AccSuccess a) -> f a x
| (AccFailure _) -> x
|AccSuccess a -> f a x
|AccFailure _ -> x

let inline traverse f = function
| (AccSuccess a) -> map AccSuccess (f a)
| (AccFailure e) -> AccFailure e
|AccSuccess a -> AccSuccess <!> f a
|AccFailure e -> result (AccFailure e)

let inline bimap f g = function
| (AccFailure e) -> AccFailure (f e)
| (AccSuccess a) -> AccSuccess (g a)
|AccFailure e -> AccFailure (f e)
|AccSuccess a -> AccSuccess (g a)

let inline bifoldr f g x = function
|(AccSuccess a) -> g a x
|(AccFailure e) -> f e x
|AccSuccess a -> g a x
|AccFailure e -> f e x

let inline bitraverse f g = function
| (AccSuccess a) -> AccSuccess (map g a)
| (AccFailure e) -> AccFailure (map f e)
| AccSuccess a -> AccSuccess <!> g a
| AccFailure e -> AccFailure <!> f e

/// | @bindValidation@ binds through an AccValidation, which is useful for
/// 'bind' binds through an AccValidation, which is useful for
/// composing AccValidations sequentially. Note that despite having a bind
/// function of the correct type, AccValidation is not a monad.
/// The reason is, this bind does not accumulate errors, so it does not
/// agree with the Applicative instance.
///
/// There is nothing wrong with using this function, it just does not make a
/// valid @Monad@ instance.
/// valid Monad instance.
let inline bind (f:'T->AccValidation<_,_>) x :AccValidation<_,_>=
match x with
| AccFailure e -> AccFailure e
| AccSuccess a -> f a

/// | @v 'orElse' a@ returns @a@ when @v@ is AccFailure, and the @a@ in @AccSuccess a@.
///
/// This can be thought of as having the less general type:
///
/// @
/// orElse :: AccValidation e a -> a -> a
/// @
let inline orElse v a =
/// orElse v a returns 'a when v is AccFailure, and the a in AccSuccess a.
let inline orElse v (a:'a) =
match v with
|AccFailure _ -> a
|AccSuccess x -> x
/// | Return the @a@ or run the given function over the @e@.
///
/// This can be thought of as having the less general type:
///
/// @
/// valueOr :: (e -> a) -> AccValidation e a -> a
/// @
//valueOr :: Validate v => (e -> a) -> v e a -> a
let valueOr ea v =
/// Return the 'a or run the given function over the 'e.
let valueOr ea (v:AccValidation<'e,'a>) =
match v with
|AccFailure e -> ea e
|AccSuccess a -> a
/// 'liftResult' is useful for converting a 'Result' to an 'AccValidation'
/// when the 'Error' of the 'Result' needs to be lifted into a 'Semigroup'.
let liftResult (f:('b -> 'e)) : (Result<'a,'b>->AccValidation<'e,'a>) = function | Error e-> AccFailure (f e) | Ok a-> AccSuccess a
/// | 'liftError' is useful for converting an 'Either' to an 'AccValidation'
/// when the @Left@ of the 'Either' needs to be lifted into a 'Semigroup'.
let liftChoice (f:('b -> 'e)) : (Either<'b,'a>->AccValidation<'e,'a>) = either (AccFailure << f) AccSuccess
/// 'liftEither' is useful for converting an 'Either' to an 'AccValidation'
/// when the 'Left' of the 'Either' needs to be lifted into a 'Semigroup'.
let liftEither (f:('b -> 'e)) : (Either<'b,'a>->AccValidation<'e,'a>) = either (AccFailure << f) AccSuccess

let inline alt a x=
match a,x with
| AccFailure _, x' -> x'
| AccSuccess a', _ -> AccSuccess a'
let appAccValidation (m:'err -> 'err -> 'err) (e1':AccValidation<'err,'a>) (e2':AccValidation<'err,'a>) =
match e1',e2' with
|AccFailure e1 , AccFailure e2 -> AccFailure (m e1 e2)
|AccFailure _ , AccSuccess a2 -> AccSuccess a2
|AccSuccess a1 , AccFailure _ -> AccSuccess a1
|AccSuccess a1 , AccSuccess _ -> AccSuccess a1

type AccValidation<'err,'a> with

// as Applicative
static member Return x = AccSuccess x
static member inline (<*>) (e1':AccValidation<'Monoid,_>, e2':AccValidation<'Monoid,_>) : AccValidation<'Monoid,_> = AccValidation.apply e1' e2'
static member inline (<*>) (f:AccValidation<_,'T->'U>, x:AccValidation<_,'T>) : AccValidation<_,_> =
AccValidation.apply f x
// as Alternative (inherits from Applicative)
static member inline get_Empty () = AccFailure ( getEmpty() )
static member inline Append (x:AccValidation<_,_>, y:AccValidation<_,_>) = AccValidation.appAccValidation FsControl.Append.Invoke x y

// as Functor
static member inline Map (x : AccValidation<_,_>, f) = AccValidation.map f x
static member inline Bind (x, f) = AccValidation.bind f x
// bimap
static member Map (x : AccValidation<_,_>, f) = AccValidation.map f x
// as Bifunctor
static member Bimap (x:AccValidation<'T,'V>, f:'T->'U, g:'V->'W) :AccValidation<'U,'W> = AccValidation.bimap f g x
//
static member inline get_Empty () = AccFailure ( getEmpty() )
//static member Append
static member inline Append (x:AccValidation<_,_>, y:AccValidation<_,_>) = AccValidation.alt x y
static member inline Traverse (t:AccValidation<_,'T>, f : 'T->AccValidation<_,'U>) : AccValidation<_,_>=AccValidation.traverse f t
// as Traversable
static member inline Traverse (t:AccValidation<'err,'a>, f : 'a->'b) : 'c=AccValidation.traverse f t

module Validations=

Expand Down
2 changes: 1 addition & 1 deletion src/Validations/Validations.fsproj
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,6 @@

<ItemGroup>
<PackageReference Include="FSharp.Core" Version="4.2.3" />
<PackageReference Include="FSharpPlus" Version="1.0.0-mci00001" />
<PackageReference Include="FSharpPlus" Version="1.0.0-CI00099" />
</ItemGroup>
</Project>
104 changes: 104 additions & 0 deletions test/Tests/PropTests.fs
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
module PropTests

open System
open Xunit
open FSharpPlus
//open FSharpPlus.Compatibility.Haskell
open Validations
open Validations.Validations // not good
open FsCheck
open FsCheck.Xunit
open FSharpPlus.Data

module FunctorP=
[<Property>]
let ``map id = id ``(x :AccValidation<string list, int>) =
(AccValidation.map id) x = id x

[<Property>]
let ``map (f << g) = map f << map g ``(x :AccValidation<string list, int>) (f:string->int) (g:int->string)=
(AccValidation.map (f << g)) x = (AccValidation.map f << AccValidation.map g) x

module BifunctorP=
[<Property>]
let ``bimap f g = first f << second g``(x :AccValidation<string, int>) (f:string->int) (g:int->string)=
(bimap f g) x = (first f << second g) x

module ApplicativeP=
///The identity law
[<Property>]
let ``result id <*> v = v``(v :AccValidation<string list, int>) =
result id <*> v = v
[<Property>]
let ``result (<<) <*> u <*> v <*> w = u <*> (v <*> w)``(v :AccValidation<string list, string->string>) (u :AccValidation<string list, string->string>) (w :AccValidation<string list, string>) =
(result (<<) <*> u <*> v <*> w) = (u <*> (v <*> w))
///Homomorphism:
[<Property>]
let ``result f <*> result x = result (f x)``(x :AccValidation<string list, int>) (f:AccValidation<string list, int> -> int) =
let y=(result (f x)):AccValidation<string list, int>
y=(result f <*> result x)
/// Interchange
/// in haskell: u <*> pure y = pure ($ y) <*> u
[<Property>]
let ``u <*> result y = result ((|>) y) <*> u``(u:AccValidation<string list, string->int> ) (y:string) =
let right_side =result ((|>) y) <*> u
let left_side = u <*> (result y)
right_side=left_side

module AlternativeP=
[<Property>]
let ``empty <|> x = x``(x :AccValidation<string list, int>) =
getEmpty() <|> x = x

[<Property>]
let ``x <|> empty = x``(x :AccValidation<string list, int>) =
x <|> getEmpty() = x

[<Property>]
let ``(x <|> y) <|> z = x <|> (y <|> z)``(x :AccValidation<string list, int>) (y :AccValidation<string list, int>) (z :AccValidation<string list, int>)=
((x <|> y) <|> z) = (x <|> (y <|> z))

[<Property>]
let ``f <!> (x <|> y) = (f <!> x) <|> (f <!> y)``(x :AccValidation<string list, int>) (y :AccValidation<string list, int>) (f:int->string)=
(f <!> (x <|> y)) = ((f <!> x) <|> (f <!> y))

//Right Distribution: does not hold
//[<Property()>]
let ``(f <|> g) <*> x = (f <*> x) <|> (g <*> x)``(x :AccValidation<string list, int>) (y :AccValidation<string list, int>) (f:AccValidation<string list,int->string>) (g:AccValidation<string list,int->string>)=
((f <|> g) <*> x) = ((f <*> x) <|> (g <*> x))

// holds when f is a function (success)
[<Property>]
let ``empty <*> f = empty ``(f:string->int)=
let empty:AccValidation<string list,_>=getEmpty()
(empty <*> (AccSuccess f))=getEmpty()

module TraversableP=

//let y_1 =traverse (fun x -> [0..x]) (AccFailure [1])
(*
[<Property>]
let ``Result: t << traverse f = traverse (t << f) ``
(x :Result<string list,string> ) (t :int->string list) (f:string list->int)=
let t_f = (t << f)
let right_side = x |> (Result.traverse (t << f))
let left_side = x |> (t << Result.traverse f )
left_side = right_side
*)
(*
[<Property>]
let ``t << traverse f = traverse (t << f) ``(x :AccValidation<string list, int>) (t :int->string) (f:string->int)=
let right_side =((traverse (t << f) x))
let left_side =(t << traverse f x)
left_side = right_side
*)
[<Property>]
let ``traverse Identity = Identity``(x :AccValidation<int list, string>)=
AccValidation.traverse (Identity) x = Identity x
(*
[<Property>]
let ``traverse (Compose << fmap g . f) = Compose << fmap (traverse g) << traverse f``(x :AccValidation<int list, string>) (g :int list->string) (f:string->int list)=
let y_1 = traverse (Compose << map (g << f))
let y_2 = Compose << map (traverse g) << traverse f
y_1 x= y_2 x
*)
47 changes: 22 additions & 25 deletions test/Tests/Tests.fsproj
Original file line number Diff line number Diff line change
@@ -1,25 +1,22 @@
<Project Sdk="Microsoft.NET.Sdk">

<PropertyGroup>
<TargetFramework>netcoreapp2.0</TargetFramework>

<IsPackable>false</IsPackable>
</PropertyGroup>

<ItemGroup>
<Compile Include="Tests.fs" />
<Compile Include="Program.fs" />
</ItemGroup>

<ItemGroup>
<PackageReference Include="FSharp.Core" Version="4.2.3" />
<PackageReference Include="Microsoft.NET.Test.Sdk" Version="15.5.0" />
<PackageReference Include="xunit" Version="2.3.1" />
<PackageReference Include="xunit.runner.visualstudio" Version="2.3.1" />
<DotNetCliToolReference Include="dotnet-xunit" Version="2.3.1" />
</ItemGroup>

<ItemGroup>
<ProjectReference Include="..\..\src\Validations\Validations.fsproj" />
</ItemGroup>
</Project>
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<TargetFramework>netcoreapp2.0</TargetFramework>
<IsPackable>false</IsPackable>
</PropertyGroup>
<ItemGroup>
<Compile Include="Tests.fs" />
<Compile Include="PropTests.fs" />
<Compile Include="Program.fs" />
</ItemGroup>
<ItemGroup>
<PackageReference Include="FSharp.Core" Version="4.2.3" />
<PackageReference Include="Microsoft.NET.Test.Sdk" Version="15.5.0" />
<PackageReference Include="xunit" Version="2.3.1" />
<PackageReference Include="xunit.runner.visualstudio" Version="2.3.1" />
<DotNetCliToolReference Include="dotnet-xunit" Version="2.3.1" />
<PackageReference Include="FsCheck.Xunit" Version="3.0.0-alpha2" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\..\src\Validations\Validations.fsproj" />
</ItemGroup>
</Project>