Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Given some inductive data type</p> <pre><code>data Nat = Succ Nat | Zero </code></pre> <p>we can consider how we pattern match on this data</p> <pre><code>case n of Succ n' -&gt; f n' Zero -&gt; g </code></pre> <p>it should be obvious that every function of type <code>Nat -&gt; a</code> can be defined by giving an appropriate <code>f</code> and <code>g</code> and that the only ways to make a <code>Nat</code> (baring bottom) is using one of the two constructors. </p> <hr> <p>EDIT: Think about <code>f</code> for a moment. If we are defining a function <code>foo :: Nat -&gt; a</code> by giving the appropriate <code>f</code> and <code>g</code> such that <code>f</code> recursively calls <code>foo</code> than we can redefine <code>f</code> as <code>f' n' (foo n')</code> such that <code>f'</code> is not recursive. If the type <code>a = (a',Nat)</code> than we can instead write <code>f' (foo n)</code>. So, without loss of generality</p> <pre><code>foo n = h $ case n Succ n' -&gt; f (foo n) Zero -&gt; g </code></pre> <p>this is the formulation that makes the rest of my post make sense:</p> <hr> <p>So, we can thus think about the case statement as applying a "destructor dictionary"</p> <pre><code>data NatDict a = NatDict { onSucc :: a -&gt; a, onZero :: a } </code></pre> <p>now our case statement from before can become</p> <pre><code>h $ case n of Succ n' -&gt; onSucc (NatDict f g) n' Zero -&gt; onZero (NatDict f g) </code></pre> <p>given this we can derive</p> <pre><code>newtype NatBB = NatBB {cataNat :: forall a. NatDict a -&gt; a} </code></pre> <p>we can then define two functions</p> <pre><code>fromBB :: NatBB -&gt; Nat fromBB n = cataNat n (NatDict Succ Zero) </code></pre> <p>and</p> <pre><code>toBB :: Nat -&gt; NatBB toBB Zero = Nat $ \dict -&gt; onZero dict toBB (Succ n) = Nat $ \dict -&gt; onSucc dict (cataNat (toBB n) dict) </code></pre> <p>we can prove these two functions are witness to an isomorphism (up to fast and lose reasoning) and thus show that</p> <pre><code>newtype NatAsFold = NatByFold (forall a. (a -&gt; a) -&gt; a -&gt; a) </code></pre> <p>(which is just the same as <code>NatBB</code>) is isomorphic to <code>Nat</code> </p> <p>We can use the same construction with other types, and prove that the resulting function types are what we want just by proving that the underlying types are isomorphic with algebraic reasoning (and induction). </p> <p>As to your second question, Haskell's type system is based on iso-recursive not equi-recursive types. This is probably becuase the theory and type inference is easier to work out with iso-recursive types, and they have all the power they just impose a little more work on the programmers part. I like to claim that you can get your iso-recursive types without any overhead</p> <pre><code>newtype RecListType a r = RecListType (r -&gt; (a -&gt; RecListType -&gt; r) -&gt; r) </code></pre> <p>but apparently GHCs optimizer chokes on those sometimes :(.</p>
    singulars
    1. This table or related slice is empty.
    1. POWhy do we use folds to encode datatypes as functions?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USPhilip JF
    1. USPhilip JF
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COWait, why is the onSucc case of the NatDict `(a -> a)`? Wouldn't it have to receive a natdict as the first argument instead of an `a` for the pattern matching parallel to hold? (The bit I still don t get is why we can be sure that the fold is just as powerful as the pattern matching in this situation)
      singulars
      1. PO
      1. UShugomg
    2. COonSucc is correct, but my later exposition is lacking...give me a moment
      singulars
      1. PO
      1. USPhilip JF
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload