Changes between Version 28 and Version 29 of PolymorphicComponents

Timestamp:

04/04/07 15:00:10 (6 years ago)

Author:

diatchki

Comment:

--

PolymorphicComponents

@@ -59 +59 @@
 = Report TODO List =
 List of items that need to change in the [http://darcs.haskell.org/haskell-prime-report/report/haskell-prime-draft.html draft report].
- 1. Introduce a new ''special identifier'', '''forall'''.  This identifier has a special interpretation in types and type schemes (i.e., it is ''not'' a type variable).
-    However, '''forall''' can still be used as an ordinary variable in expressions.
- 2. Syntax for writing type schemes:
-    (TODO: check for ambiguities with happy.)
+
+== Syntax ==
+Introduce a new ''special identifier'', '''forall'''.  This identifier has a special interpretation in types and type schemes (i.e., it is ''not'' a type variable).
+However, '''forall''' can still be used as an ordinary variable in expressions.
+
+Syntax for writing type schemes:
 {{{
 poly     -> 'forall' tvar_1 ... tyvar_n '.' opt_ctxt type    (n > 0)
@@ -71 +73 @@
 bscheme  -> '(' poly ')' | btype
 }}}
- NOTE: Schemes should not contain quantified variables that are not mentioned
-       in the scheme body because this probably indicates a programmer error.
- 3. Syntax for '''data''' and '''newtype''' declarations 
+NOTE: Schemes should not contain quantified variables that are not mentioned in the scheme body because this probably indicates a programmer error.
+
+Syntax for '''data''' and '''newtype''' declarations 
 {{{
 -- Section 4.2.1
@@ -89 +91 @@
           | con { var :: scheme }
 }}}
- NOTE: The grammar in the Haskell 98 report contains a minor bug that seems
- to allow erroneous data declarations like the following:
+NOTE: The grammar in the Haskell 98 report contains a minor bug that seems
+to allow erroneous data declarations like the following:
 {{{
 data T = C !
 }}}
- For this reason I introduced the ''con_field'' productions.
- 4. Labeled fields.  
-   1. Type of the selector functions:
+For this reason I introduced the ''con_field'' productions.
+
+== Working with datatypes ==
+
+=== Labeled fields ===
+
+Type of the selector functions:
 {{{
 data T a = C { x :: forall b. ctxt  => type }
 x :: ctxt => T a -> type
 }}}
-   2. If different constructors of the same datatype contain the same label,
-    then the      corresponding schemes should be equal up to renaming of the
-    quantified variables.
 
+If different constructors of the same datatype contain the same label,
+then the corresponding schemes should be equal up to renaming of the
+quantified variables.  This ensures that we can give a reasonable type
+for the selector functions.
+
+=== Constructors ===
+
+Constructors that have polymorphic components cannot appear in the program
+without values for their polymorphic fields. For example,
+consider the following declaration:
+{{{
+data T a  = C Int (forall b. b -> a) a
+}}}
+The constructor function 'C' cannot be used with less then two arguments
+because the second argument is the last polymorphic component of 'C'.
+Here are some examples that illustrate what we can and cannot do with 'C':
+{{{
+ex1 :: a -> T a
+ex1 a = C 2 (const a)      -- ok.
+
+ex2 = C 2                  -- not ok, needs another argument.
+}}}
+This restriction ensures that all expressions in the program have
+ordinary Hindley-Milner types.
+
+The values for the polymorphic components should have type schemes
+that are at least as polymorphic as what is declared in the datatype.
+This is checked is similar to the check that is performed when an
+expression has an explicit type signature.
 
 TODO:
@@ -110 +142 @@
  1. english text in Labelled fields - give an example of fields with polymorphic types, or do this in section 3?
  1. anything in "kind inference"?
- 1. ''note for'': for field labels, when you have the same label in different constructors, it's permitted as long as the type is the same; anything here to describe the syntactic checking that occurs to determine whether these types are the same?  "Syntactic up-to alpha-renaming." Might be unintuative as this is rejected by GHC and Hugs:
-{{{
-data T  = C1 { x :: forall a. (Show a,Eq a) => a -> a }
-        | C2 { x :: forall a. (Eq a,Show a) => a -> a } 
-}}}
  1. ''note'' you can name polymorphic components (see design choice above)
    1. when you match on ''x'' it instantiates the forall to a monomorphic type as below: