1. David Barker
  2. C# Arrows

Commits

David Barker  committed 437d3f1

Wrote up invertible arrow laws

  • Participants
  • Parent commits 46a2e14
  • Branches master

Comments (0)

Files changed (18)

File ArrowDataBinding.v11.suo

  • Ignore whitespace
Binary file modified.

File Dissertation/Dissertation.log

View file
  • Ignore whitespace
-This is pdfTeX, Version 3.1415926-2.3-1.40.12 (MiKTeX 2.9 64-bit) (preloaded format=pdflatex 2012.10.5)  28 APR 2013 14:59
+This is pdfTeX, Version 3.1415926-2.3-1.40.12 (MiKTeX 2.9 64-bit) (preloaded format=pdflatex 2012.10.5)  29 APR 2013 13:55
 entering extended mode
 **Dissertation.tex
 
 \pc@column@2=\box30
 \pc@column@width@2=\dimen120
 Package parcolumns Info: Width of column 1 calculated as 194.2195pt on input li
-ne 884.
+ne 924.
 Package parcolumns Info: Width of column 2 calculated as 194.2195pt on input li
-ne 884.
+ne 924.
 [43
 
 ]
 Package parcolumns Info: Width of column 1 calculated as 194.2195pt on input li
-ne 939.
+ne 979.
 Package parcolumns Info: Width of column 2 calculated as 194.2195pt on input li
-ne 939.
+ne 979.
  [44]
 Package parcolumns Info: Width of column 1 calculated as 194.2195pt on input li
-ne 984.
+ne 1024.
 Package parcolumns Info: Width of column 2 calculated as 194.2195pt on input li
-ne 984.
+ne 1024.
  [45] [46]
 Package parcolumns Info: Width of column 1 calculated as 194.2195pt on input li
-ne 1026.
+ne 1066.
 Package parcolumns Info: Width of column 2 calculated as 194.2195pt on input li
-ne 1026.
+ne 1066.
  [47
 
 ]
 Package parcolumns Info: Width of column 1 calculated as 194.2195pt on input li
-ne 1068.
+ne 1108.
 Package parcolumns Info: Width of column 2 calculated as 194.2195pt on input li
-ne 1068.
+ne 1108.
  [48] [49
 
 ] [50
 ("C:\Users\David\Documents\Visual Studio 2010\Projects\ArrowDataBinding\Dissert
 ation\Dissertation.aux") ) 
 Here is how much of TeX's memory you used:
- 2946 strings out of 494045
- 43403 string characters out of 3148387
- 216622 words of memory out of 3000000
- 6216 multiletter control sequences out of 15000+200000
+ 2968 strings out of 494045
+ 43643 string characters out of 3148387
+ 271622 words of memory out of 3000000
+ 6238 multiletter control sequences out of 15000+200000
  12938 words of font info for 46 fonts, out of 3000000 for 9000
  715 hyphenation exceptions out of 8191
  27i,8n,40p,1132b,1520s stack positions out of 5000i,500n,10000p,200000b,50000s
 ogram Files/MiKTeX 2.9/fonts/type1/public/amsfonts/cm/cmtt10.pfb><C:/Program Fi
 les/MiKTeX 2.9/fonts/type1/public/amsfonts/cm/cmtt12.pfb><C:/Program Files/MiKT
 eX 2.9/fonts/type1/public/amsfonts/cm/cmtt8.pfb>
-Output written on Dissertation.pdf (62 pages, 556197 bytes).
+Output written on Dissertation.pdf (62 pages, 558058 bytes).
 PDF statistics:
  619 PDF objects out of 1000 (max. 8388607)
  0 named destinations out of 1000 (max. 500000)

File Dissertation/Dissertation.pdf

  • Ignore whitespace
Binary file modified.

File Dissertation/Dissertation.synctex.gz

  • Ignore whitespace
Binary file modified.

File Dissertation/Dissertation.tex

View file
  • Ignore whitespace
 
 As invertible arrows conform to a slightly different set of arrow laws (which put extra requirements on their inverses), both one-way arrows and invertible arrows had to be tested separately. List and choice arrows were not separately tested as they are entirely built upon normal one-way arrows, and so will conform to the arrow laws for free if simple arrows do.
 
-[Mention correctness proof by decomposition into lambda calculus?]
+%Mention correctness proof by decomposition into lambda calculus?
 
 \subsection{Automated testing}
 
 
 This defines a \texttt{Func} which invokes a function 'f' on the first element of a tuple.
 
+The relation `$\approx$' is used throughout to relate effectively equivalent C$\sharp$ expressions.
+
 \section{Normal arrow laws} \label{sec:simle_arrow_laws}
 
 \begin{samepage}
 
 \section{Invertible arrow laws} \label{sec:invertible_arrow_laws}
 
-Todo
+\begin{samepage}
+\begin{lstlisting}[mathescape]
+Composition associativity
+f >>> (g >>> h) = (f >>> g) >>> h
+f.Combine(g.Combine(h)) $\approx$ (f.Combine(g)).Combine(h)
+
+Composition distributivity
+f1 $\leftrightarrow$ g2 >>> g1 $\leftrightarrow$ f2 = (f1 >>> g1) $\leftrightarrow$ (f2 >>> g2)
+f1.Arr(g2).Combine(g1.Arr(f2)) $\approx$ Op.Arr(x => g1(f1(x)), y => g2(f2(x)))
+
+Composition with identity
+idA >>> f = f = f >>> idA  (where idA = id $\leftrightarrow$ id)
+new IDArrow<T>().Combine(f) $\approx$ f $\approx$ f.Combine(new IDArrow<T>())
+
+`First' operator distributivity
+first (f >>> g) = first f >>> first g
+(f.Combine(g)).First<T>() $\approx$ first_f.Combine(first_g)
+
+`First' operator commutativity
+first (f $\leftrightarrow$ g) = (f * id) $\leftrightarrow$ (g * id)
+(f.Arr(g)).First<T>() $\approx$ f.Mult(id).Arr(g.Mult(id))
+
+Double inversion
+inv (inv f) = f
+f.Invert().Invert() $\approx$ f
+
+Distributivity of inversion
+inf (f >>> g) = inv g >>> inv f
+f.Combine(g).Invert() $\approx$ g.Invert().Combine(f.Invert())
+
+Inversion correctness
+inv (f $\leftrightarrow$ g) = g $\leftrightarrow$ f
+f.Arr(g).Invert() $\approx$ g.Arr(f)
+
+`First' operator under inversion
+inv (first f) = first (inv f)
+f.First<T>().Invert() $\approx$ f.Invert().First<T>()
+\end{lstlisting}
+\end{samepage}
 
 \cleardoublepage
 

File WPFIntegrationDemo/MainWindow.xaml

View file
  • Ignore whitespace
     <Grid>
         <TextBlock x:Name="TextBox" HorizontalAlignment="Left" Margin="23,27,0,0" TextWrapping="Wrap" Text="TextBlock" VerticalAlignment="Top" Height="48" Width="458"/>
         <ProgressBar x:Name="Progress" HorizontalAlignment="Left" Height="40" Margin="23,80,0,0" VerticalAlignment="Top" Width="450"/>
+        <TextBlock x:Name="TimerLabel" HorizontalAlignment="Left" Margin="43,213,0,0" VerticalAlignment="Top"/>
 
     </Grid>
 </Window>

File WPFIntegrationDemo/MainWindow.xaml.cs

View file
  • Ignore whitespace
         {
             InitialiseTextBinding();
             InitialiseProgressBarBinding();
+            InitialiseTimerBinding();
         }
 
         public void InitialiseTextBinding()
             binding.Converter = new ArrowValueConverter(progressArrow);
             Progress.SetBinding(ProgressBar.ValueProperty, binding);
         }
+
+        public void InitialiseTimerBinding()
+        {
+            Binding binding = new Binding();
+            binding.Source = time;
+            binding.Mode = BindingMode.OneWay;
+            binding.Path = new PropertyPath("CurrentTime");
+            TimerLabel.SetBinding(TextBlock.TextProperty, binding);
+        }
     }
 
     public class Time : Bindable

File WPFIntegrationDemo/bin/Debug/WPFIntegrationDemo.exe

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/bin/Debug/WPFIntegrationDemo.pdb

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/bin/Debug/WPFIntegrationDemo.pssym

View file
  • Ignore whitespace
 <?xml version="1.0" encoding="utf-8"?>
 <Symbols xmlns="http://schemas.postsharp.org/2.0/symbols">
-  <Class Class="#1=T:[ArrowDataBinding]ArrowDataBinding.Bindings.BindableAttribute" LimitedLicense="true" />
+  <Class Class="#1=T:[ArrowDataBinding]ArrowDataBinding.Bindings.BindableAttribute">
+    <Instance Declaration="#2=P:[WPFIntegrationDemo]WPFIntegrationDemo.Time::CurrentTime()" Id="7b87e4ac773b7c8c">
+      <Target>
+        <JoinPoint Advised="#3=M:[WPFIntegrationDemo]WPFIntegrationDemo.Time::get_CurrentTime()" Advising="#1" Description="#4=Intercepted by advice OnGetValue" Semantic="Getter" />
+        <JoinPoint Advised="#5=M:[WPFIntegrationDemo]WPFIntegrationDemo.Time::set_CurrentTime(System.Int32)" Advising="#1" Description="#6=Intercepted by advice OnSetValue" Semantic="Setter" />
+      </Target>
+    </Instance>
+  </Class>
 </Symbols>

File WPFIntegrationDemo/obj/Debug/Before-PostSharp/WPFIntegrationDemo.exe

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/obj/Debug/Before-PostSharp/WPFIntegrationDemo.pdb

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/obj/Debug/MainWindow.baml

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/obj/Debug/MainWindow.g.cs

View file
  • Ignore whitespace
-#pragma checksum "..\..\MainWindow.xaml" "{406ea660-64cf-4c82-b6f0-42d48172a799}" "C499077D5D8E96CEBBCE355D8D68CBA3"
+#pragma checksum "..\..\MainWindow.xaml" "{406ea660-64cf-4c82-b6f0-42d48172a799}" "04474A4DCB7BB37911C3C2F9E6AD0F27"
 //------------------------------------------------------------------------------
 // <auto-generated>
 //     This code was generated by a tool.
         #line default
         #line hidden
         
+        
+        #line 8 "..\..\MainWindow.xaml"
+        [System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1823:AvoidUnusedPrivateFields")]
+        internal System.Windows.Controls.TextBlock TimerLabel;
+        
+        #line default
+        #line hidden
+        
         private bool _contentLoaded;
         
         /// <summary>
             case 2:
             this.Progress = ((System.Windows.Controls.ProgressBar)(target));
             return;
+            case 3:
+            this.TimerLabel = ((System.Windows.Controls.TextBlock)(target));
+            return;
             }
             this._contentLoaded = true;
         }

File WPFIntegrationDemo/obj/Debug/MainWindow.g.i.cs

View file
  • Ignore whitespace
-#pragma checksum "..\..\MainWindow.xaml" "{406ea660-64cf-4c82-b6f0-42d48172a799}" "C499077D5D8E96CEBBCE355D8D68CBA3"
+#pragma checksum "..\..\MainWindow.xaml" "{406ea660-64cf-4c82-b6f0-42d48172a799}" "04474A4DCB7BB37911C3C2F9E6AD0F27"
 //------------------------------------------------------------------------------
 // <auto-generated>
 //     This code was generated by a tool.
         #line default
         #line hidden
         
+        
+        #line 8 "..\..\MainWindow.xaml"
+        [System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1823:AvoidUnusedPrivateFields")]
+        internal System.Windows.Controls.TextBlock TimerLabel;
+        
+        #line default
+        #line hidden
+        
         private bool _contentLoaded;
         
         /// <summary>
             case 2:
             this.Progress = ((System.Windows.Controls.ProgressBar)(target));
             return;
+            case 3:
+            this.TimerLabel = ((System.Windows.Controls.TextBlock)(target));
+            return;
             }
             this._contentLoaded = true;
         }

File WPFIntegrationDemo/obj/Debug/WPFIntegrationDemo.exe

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/obj/Debug/WPFIntegrationDemo.g.resources

  • Ignore whitespace
Binary file modified.

File WPFIntegrationDemo/obj/Debug/WPFIntegrationDemo.pdb

  • Ignore whitespace
Binary file modified.