Tidy up

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, Z>) : Z = Unchecked.defaultof<_>
+    static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S<S<Add< ^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<_>
+

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, Z>) : Z = Unchecked.defaultof<_>
-    static member inline refine< ^n1, ^n2> (_ : Add< S< ^n1>, S< ^n2>>) : S<S<Add< ^n1, ^n2>>> = 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.
+[<Struct>]
+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 =
 
 [<RequireQualifiedAccess>]
 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
+    [<RequireQualifiedAccess>]
+    module Unsafe =
+        let cast<'a, 'n, 'm> (Vector a : Vector<'a, 'n>) : Vector<'a, 'm> = Vector a
+
+    /// Allows you to convert safely between Vector<int, 3> and Vector<int, 1 + 2>, 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
 
 [<AutoOpen>]
 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>) = ()

Vector/Vector.fsproj

@@ -5,6 +5,7 @@
     </PropertyGroup>
 
     <ItemGroup>
+        <Compile Include="Arithmetic.fs" />
         <Compile Include="Vector.fs" />
     </ItemGroup>