Merge pull request #1 from purescript/docs

Documentation

Author: paf31

Gruntfile.js

@@ -34,6 +34,13 @@ module.exports = function(grunt) {
       }
     ],
 
+    pscDocs: {
+      readme: {
+        src: "src/**/*.purs",
+        dest: "README.md"
+      }
+    },
+
     execute: {
       tests: {
         src: "tmp/index.js"
@@ -47,6 +54,6 @@ module.exports = function(grunt) {
   grunt.loadNpmTasks("grunt-purescript");
 
   grunt.registerTask("test", ["pscMake:tests", "copy", "execute:tests"]);
-  grunt.registerTask("make", ["pscMake:lib", "dotPsci"]);
+  grunt.registerTask("make", ["pscMake:lib", "dotPsci", "pscDocs"]);
   grunt.registerTask("default", ["clean", "make", "test"]);
 };

README.md

@@ -1,11 +1,68 @@
-# purescript-exists
+# Module Documentation
 
-Existential types as a library
+## Module Data.Exists
 
-## Building
+#### `Exists`
 
+``` purescript
+data Exists :: (* -> *) -> *
 ```
-npm install
-bower update
-grunt
+
+This type constructor can be used to existentially quantify over a type of kind `*`.
+
+Specifically, the type `Exists f` is isomorphic to the existential type `exists a. f a`.
+
+Existential types can be encoded using universal types (`forall`) for endofunctors in more general
+categories. The benefit of this library is that, by using the FFI, we can create an efficient
+representation of the existential by simply hiding type information.
+
+For example, consider the type `exists s. Tuple s (s -> Tuple s a)` which represents infinite streams
+of elements of type `a`.
+
+This type can be constructed by creating a type constructor `StreamF` as follows:
+
+```purescript
+data StreamF a s = StreamF s (s -> Tuple s a) 
+```
+
+We can then define the type of streams using `Exists`:
+
+```purescript
+type Stream a = Exists (StreamF a)
+```
+
+#### `mkExists`
+
+``` purescript
+mkExists :: forall f a. f a -> Exists f
+```
+
+The `mkExists` function is used to introduce a value of type `Exists f`, by providing a value of
+type `f a`, for some type `a` which will be hidden in the existentially-quantified type.
+
+For example, to create a value of type `Stream Number`, we might use `mkExists` as follows:
+
+```purescript
+nats :: Stream Number
+nats = mkExists $ StreamF 0 (\n -> Tuple (n + 1) n)
 ```
+
+#### `runExists`
+
+``` purescript
+runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r
+```
+
+The `runExists` function is used to eliminate a value of type `Exists f`. The rank 2 type ensures
+that the existentially-quantified type does not escape its scope. Since the function is required
+to work for _any_ type `a`, it will work for the existentially-quantified type.
+
+For example, we can write a function to obtain the head of a stream by using `runExists` as follows:
+
+```purescript
+head :: forall a. Stream a -> a
+head = runExists head'
+  where
+  head' :: forall s. StreamF a s -> a
+  head' (StreamF s f) = snd (f s) 
+```

package.json

@@ -11,6 +11,6 @@
     "grunt-contrib-copy": "~0.5.0",
     "grunt-contrib-clean": "~0.5.0",
     "grunt-execute": "~0.1.5",
-    "grunt-purescript": "~0.5.0"
+    "grunt-purescript": "~0.6.0"
   }
 }

src/Data/Exists.purs

@@ -1,12 +1,56 @@
 module Data.Exists where
 
+-- | This type constructor can be used to existentially quantify over a type of kind `*`.
+-- |
+-- | Specifically, the type `Exists f` is isomorphic to the existential type `exists a. f a`.
+-- |
+-- | Existential types can be encoded using universal types (`forall`) for endofunctors in more general
+-- | categories. The benefit of this library is that, by using the FFI, we can create an efficient
+-- | representation of the existential by simply hiding type information.
+-- |
+-- | For example, consider the type `exists s. Tuple s (s -> Tuple s a)` which represents infinite streams
+-- | of elements of type `a`.
+-- |
+-- | This type can be constructed by creating a type constructor `StreamF` as follows:
+-- |
+-- | ```purescript
+-- | data StreamF a s = StreamF s (s -> Tuple s a) 
+-- | ```
+-- |
+-- | We can then define the type of streams using `Exists`:
+-- |
+-- | ```purescript
+-- | type Stream a = Exists (StreamF a)
+-- | ```
 foreign import data Exists :: (* -> *) -> *
- 
+
+-- | The `mkExists` function is used to introduce a value of type `Exists f`, by providing a value of
+-- | type `f a`, for some type `a` which will be hidden in the existentially-quantified type.
+-- |
+-- | For example, to create a value of type `Stream Number`, we might use `mkExists` as follows:
+-- |
+-- | ```purescript
+-- | nats :: Stream Number
+-- | nats = mkExists $ StreamF 0 (\n -> Tuple (n + 1) n)
+-- | ```
 foreign import mkExists
   "function mkExists(fa) {\
   \  return fa;\
   \}" :: forall f a. f a -> Exists f
-  
+ 
+-- | The `runExists` function is used to eliminate a value of type `Exists f`. The rank 2 type ensures
+-- | that the existentially-quantified type does not escape its scope. Since the function is required
+-- | to work for _any_ type `a`, it will work for the existentially-quantified type.
+-- | 
+-- | For example, we can write a function to obtain the head of a stream by using `runExists` as follows:
+-- | 
+-- | ```purescript
+-- | head :: forall a. Stream a -> a
+-- | head = runExists head'
+-- |   where
+-- |   head' :: forall s. StreamF a s -> a
+-- |   head' (StreamF s f) = snd (f s) 
+-- | ```
 foreign import runExists
   "function runExists(f) {\
   \  return function(fa) {\

tests/Tests.purs

@@ -3,11 +3,22 @@ module Main where
 import Debug.Trace
 import Data.Exists
 
-data Example a = Example a (a -> String)
- 
-runExample :: Exists Example -> String
-runExample = runExists (\(Example a f) -> f a)
- 
-test = runExample (mkExists (Example "Done" show))
-
-main = trace test
+data Tuple a b = Tuple a b
+
+snd :: forall a b. Tuple a b -> b
+snd (Tuple _ b) = b
+
+data StreamF a s = StreamF s (s -> Tuple s a) 
+
+type Stream a = Exists (StreamF a)
+
+nats :: Stream Number
+nats = mkExists $ StreamF 0 (\n -> Tuple (n + 1) n)
+
+head :: forall a. Stream a -> a
+head = runExists head'
+  where
+  head' :: forall s. StreamF a s -> a
+  head' (StreamF s f) = snd (f s) 
+
+main = print $ head nats