diff --git a/Vector.Test/UnitTest1.fs b/Vector.Test/TestVector.fs similarity index 64% rename from Vector.Test/UnitTest1.fs rename to Vector.Test/TestVector.fs index ec118df..1616b3d 100644 --- a/Vector.Test/UnitTest1.fs +++ b/Vector.Test/TestVector.fs @@ -7,7 +7,7 @@ open FsUnitTyped [] module TestVector = [] - let example1 () = + let ``Basic construction`` () = let v1 = Vector.empty |> Vector.cons 3 @@ -18,15 +18,32 @@ module TestVector = let v2 = Vector.empty |> Vector.cons "hi" |> Vector.cons "bye" v2 |> Vector.toList |> shouldEqual ["bye" ; "hi"] + [] + let ``Pattern matching`` () = match Vector.empty with | Empty () -> () //| Vec (a, b) -> failwith "" -- doesn't compile + let v1 = + Vector.empty + |> Vector.cons 3 + |> Vector.cons 5 + |> Vector.cons 6 + match v1 with | Vec (a , b) -> a |> shouldEqual 6 - b |> Vector.toList |> shouldEqual [5 ; 3] + match b with + | Vec (b, c) -> + b |> shouldEqual 5 + match c with + | Vec (c, d) -> + c |> shouldEqual 3 + match d with + | Empty () -> () + [] + let ``Vector concatenation`` () = let v1 = Vector.empty |> Vector.cons 3 @@ -43,24 +60,16 @@ module TestVector = |> Vector.cons 5 |> Vector.cons 6 + // They are equal vectors... twice |> Vector.toList |> shouldEqual (otherTwice |> Vector.toList) + // but their equality doesn't typecheck. + // twice |> shouldEqual otherTwice + // But sufficient safe casting can make it typecheck. twice |> Vector.cast |> Vector.cast |> Vector.cast |> Vector.cast |> shouldEqual otherTwice - - [] - let foo () = - let v1 = Vector.empty |> Vector.cons 1 - let twice = Vector.append v1 v1 - let twiceAgain = Vector.empty |> Vector.cons 1 |> Vector.cons 1 - - twice - |> Vector.cast - |> Vector.cast - |> shouldEqual twiceAgain - diff --git a/Vector.Test/Vector.Test.fsproj b/Vector.Test/Vector.Test.fsproj index 6941849..9d9b7ef 100644 --- a/Vector.Test/Vector.Test.fsproj +++ b/Vector.Test/Vector.Test.fsproj @@ -15,7 +15,7 @@ - + diff --git a/Vector/Arithmetic.fs b/Vector/Arithmetic.fs new file mode 100644 index 0000000..96a7ba8 --- /dev/null +++ b/Vector/Arithmetic.fs @@ -0,0 +1,24 @@ +namespace Vector.Naturals + +/// Zero, in the Peano encoding of the naturals +type Z = + private + | Z + +/// Successor, in the Peano encoding of the naturals +type S<'a> = + private + | S + // Computation rules + static member inline refine< ^n1, ^n2 when ^n1 : (static member refine : ^n1 -> ^n2)> (_ : S<'n1>) : S<'n2> = Unchecked.defaultof<_> + +/// Type representing the sum of two naturals +type Add<'a, 'b> = + private + | Add + // Computation rules + static member inline refine (_ : Add) : Z = Unchecked.defaultof<_> + static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S>> = Unchecked.defaultof<_> + static member inline refine< ^n1, ^n2> (_ : Add< Z, ^n1>) : ^n2 = Unchecked.defaultof<_> + static member inline refine< ^n1, ^n2 > (_ : Add< ^n1, Z>) : ^n2 = Unchecked.defaultof<_> + diff --git a/Vector/Vector.fs b/Vector/Vector.fs index 22931f4..3675cb8 100644 --- a/Vector/Vector.fs +++ b/Vector/Vector.fs @@ -1,29 +1,10 @@ -namespace Vector +namespace Vector -type Z = - private - | Z - static member computed (_ : Z) : unit = () +open Vector.Naturals -type S<'a> = - private - | S - static member inline refine< ^n1, ^n2 when ^n1 : (static member refine : ^n1 -> ^n2)> (_ : S<'n1>) : S<'n2> = Unchecked.defaultof<_> - static member inline computed< ^n1 when ^n1 : (static member computed : ^n1 -> unit)> (_ : S<'n1>) : unit = () - -type Add<'a, 'b> = - private - | Add - static member inline refine (_ : Add) : Z = Unchecked.defaultof<_> - static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S>> = Unchecked.defaultof<_> - //static member inline refine< ^n1, ^n2 when (^n1 or ^n2) : (static member refine : ^n1 -> ^n2)> (_ : Add< Z, ^n1>) : ^n2 = Unchecked.defaultof<_> - static member inline refine< ^n1, ^n2> (_ : Add< Z, ^n1>) : ^n2 = Unchecked.defaultof<_> - static member inline refine< ^n1, ^n2 > (_ : Add< ^n1, Z>) : ^n2 = Unchecked.defaultof<_> - -type Vector<'a, 'len> = - { - Elements : 'a list - } +/// A vector with known length. +[] +type Vector<'a, 'len> = private | Vector of 'a list type VectorCrateEvaluator<'a, 'ret> = abstract Eval<'n> : Vector<'a, 'n> -> 'ret type VectorCrate<'a> = abstract Apply<'ret> : VectorCrateEvaluator<'a, 'ret> -> 'ret @@ -37,15 +18,15 @@ module VectorCrate = [] module Vector = - let empty<'a> : Vector<'a, Z> = { Elements = [] } + let empty<'a> : Vector<'a, Z> = Vector [] - let cons<'a, 'n> (x : 'a) (v : Vector<'a, 'n>) : Vector<'a, S<'n>> = - { - Elements = x :: v.Elements - } + let cons<'a, 'n> (x : 'a) (Vector v : Vector<'a, 'n>) : Vector<'a, S<'n>> = + Vector (x :: v) - let toList<'a, 'n> (v : Vector<'a, 'n>) : 'a list = v.Elements + let toList<'a, 'n> (Vector v : Vector<'a, 'n>) : 'a list = v + /// This is very inefficient, and I can't imagine it being helpful, + /// but it's here for completeness. let rec ofList<'a> (v : List<'a>) : VectorCrate<'a> = match v with | [] -> VectorCrate.make empty @@ -59,32 +40,38 @@ module Vector = } } - let append<'a, 'n1, 'n2> (v1 : Vector<'a, 'n1>) (v2 : Vector<'a, 'n2>) : Vector<'a, Add<'n1, 'n2>> = - { Elements = List.append v1.Elements v2.Elements } + /// Vector.append v1 v2 is v1 ++ v2. (Which is a bit sad, given how often we would want to pipe this, + /// but it's consistent with List.) + let append<'a, 'n1, 'n2> (Vector v1 : Vector<'a, 'n1>) (Vector v2 : Vector<'a, 'n2>) : Vector<'a, Add<'n1, 'n2>> = + List.append v1 v2 + |> Vector - let fold<'a, 's, 'n> (f : 's -> 'a -> 's) (s : 's) (v : Vector<'a, 'n>) = - List.fold f s v.Elements + let fold<'a, 's, 'n> (f : 's -> 'a -> 's) (s : 's) (Vector v : Vector<'a, 'n>) = + List.fold f s v - let zip<'a, 'b, 'n> (v1 : Vector<'a, 'n>) (v2 : Vector<'b, 'n>) : Vector<'a * 'b, 'n> = - { - Elements = List.zip v1.Elements v2.Elements - } + let zip<'a, 'b, 'n> (Vector v1 : Vector<'a, 'n>) (Vector v2 : Vector<'b, 'n>) : Vector<'a * 'b, 'n> = + List.zip v1 v2 + |> Vector - let map<'a, 'b, 'n> (f : 'a -> 'b) (v : Vector<'a, 'n>) : Vector<'b, 'n> = - { - Elements = List.map f v.Elements - } + let map<'a, 'b, 'n> (f : 'a -> 'b) (Vector v : Vector<'a, 'n>) : Vector<'b, 'n> = + List.map f v + |> Vector - let head<'a, 'n> (v : Vector<'a, S<'n>>) : 'a = v.Elements.[0] - let tail<'a, 'n> (v : Vector<'a, S<'n>>) : Vector<'a, 'n> = { Elements = List.tail v.Elements } - let unsafeCast<'a, 'n, 'm> (a : Vector<'a, 'n>) : Vector<'a, 'm> = { Elements = a.Elements } + let head<'a, 'n> (Vector v : Vector<'a, S<'n>>) : 'a = List.head v + let tail<'a, 'n> (Vector v : Vector<'a, S<'n>>) : Vector<'a, 'n> = List.tail v |> Vector - let inline cast< ^n2, ^n1, 'a when (^n1 or ^n2) : (static member refine : ^n1 -> ^n2)> (a : Vector<'a, ^n1>) : Vector<'a, ^n2> = unsafeCast a - let inline cast'< ^n1, ^n2, 'a when (^n1 or ^n2) : (static member refine : ^n1 -> ^n2)> (a : Vector<'a, ^n1>) : Vector<'a, ^n2> = unsafeCast a + [] + module Unsafe = + let cast<'a, 'n, 'm> (Vector a : Vector<'a, 'n>) : Vector<'a, 'm> = Vector a + + /// Allows you to convert safely between Vector and Vector, say. + /// You may need to call `cast` multiple times. + let inline cast< ^n2, ^n1, 'a when (^n1 or ^n2) : (static member refine : ^n1 -> ^n2)> (a : Vector<'a, ^n1>) : Vector<'a, ^n2> = Unsafe.cast a + let inline cast'< ^n1, ^n2, 'a when (^n1 or ^n2) : (static member refine : ^n1 -> ^n2)> (a : Vector<'a, ^n1>) : Vector<'a, ^n2> = Unsafe.cast a [] module Patterns = - let (|Vec|) (v : Vector<'a, S<'n>>) : 'a * Vector<'a, 'n> = - List.head v.Elements, { Elements = List.tail v.Elements } + let (|Vec|) (Vector v : Vector<'a, S<'n>>) : 'a * Vector<'a, 'n> = + List.head v, Vector (List.tail v) let (|Empty|) (_ : Vector<'a, Z>) = () \ No newline at end of file diff --git a/Vector/Vector.fsproj b/Vector/Vector.fsproj index 9eede08..fde8273 100644 --- a/Vector/Vector.fsproj +++ b/Vector/Vector.fsproj @@ -5,6 +5,7 @@ +