2 | | |
3 | | These are some rough and unfinished notes about the details of |
4 | | adding polymorphic components to datatypes. |
5 | | |
6 | | == Notation == |
7 | | |
8 | | We need a notation to write the type schemes for polymorphic components. |
9 | | Hugs and GHC differ slightly in their choice of notation. |
10 | | |
11 | | |
12 | | === Recognizing Schemes === |
13 | | |
14 | | We use 'forall' To indicate that a field in a constructor of a |
15 | | 'data' or a 'newtype' declaration is polymorphic. |
16 | | In Hugs, 'forall' is implemented as a new keyword, while in GHC it |
17 | | is a "special" identifier that is treated differently in contexts |
18 | | that expect a type and in contexts that expect values. For example, |
19 | | the following definitions is rejected by Hugs but accepted by GHC: |
20 | | {{{ |
21 | | f forall = forall |
22 | | }}} |
23 | | PROPOSAL: adopt GHC's convention and treat 'forall' specially in |
24 | | types but allow it to be used in value declarations. |
25 | | |
26 | | |
27 | | === Notation for Schemes === |
28 | | |
29 | | {{{ |
30 | | scheme = 'forall' tvars '.' opt_ctxt type |
31 | | |
32 | | opt_ctxt = context '=>' |
33 | | | |
34 | | }}} |
35 | | |
36 | | The non-terminal 'tvars' is a sequence of type variables that are |
37 | | separated by blank spaces. We have a choice if we should allow |
38 | | empty quantifier sequences. |
39 | | |
40 | | ==== Some static checking ==== |
41 | | Here are some differences between Hugs and GHC: |
42 | | |
43 | | Hugs: |
44 | | * does not allow empty quantifier lists |
45 | | * requires that variables are mentioned in the body of a type |
46 | | * permits predicates that do not mention any of the quantified variables |
47 | | |
48 | | GHC: |
49 | | * allows empty quantifiers |
50 | | * warns when quantified variables are not mentioned the body of a type |
51 | | * disallows predicates that do not mention any of the quantified variables |
52 | | |
53 | | PROPOSAL: be liberal: |
54 | | * allow empty quantifier lists |
55 | | * allow variables that are not mentioned in the body of a type (but warn) |
56 | | * allow predicates that do not mention quantified variables (but warn?) |
57 | | |
58 | | |
59 | | === Strict Fields === |
60 | | |
61 | | The fields in 'data' constructors may be annotated with '!', indicating |
62 | | that they are strict. Where should we place the '!' for a polymorphic field? |
63 | | It appears that this is not supported in Hugs (bug? I have not looked at |
64 | | the parser). In GHC, the '!' is placed before a schema and the schema has to |
65 | | be in parens (i.e. syntactically, a schema is just another 'type'). |
66 | | |
67 | | Example: |
68 | | {{{ |
69 | | data T = C !(forall a. a -> a) Int |
70 | | }}} |
71 | | PROPOSAL: GHC's choice seems reasonable. |
72 | | |
73 | | === Labeled Fields, Infix Constructors === |
74 | | |
75 | | Again, we treat schemes as if they belong to category 'type'. |
76 | | |
77 | | Examples: |
78 | | {{{ |
79 | | data T = C { f1 :: forall a. a -> a, f2 :: Int } |
80 | | data T = (forall a. a -> a) :+: (forall x. x -> x) |
81 | | }}} |
82 | | In the second example we need the parens to turn 'type' into 'atype'. |
83 | | |
84 | | One issue with labelled fields is that Haskell 98 requers that if a label appears in different constructors of a datatype, then the labelled fields should have the same type. In the presences of polymorphic components, this translates to deciding if two schemas are equal, so we need to decide how that should work. It seems that at present, Hugs and GHC consider two schemas to be the same if they are syntactically the same (up to alpha renaming). |
85 | | |
86 | | Examples: |
87 | | {{{ |
88 | | forall a. a -> a |
89 | | === |
90 | | forall b. b -> b |
91 | | }}} |
92 | | {{{ |
93 | | forall a. (Eq a, Show a) => a -> a |
94 | | =/= |
95 | | forall a. (Show a, Eq a) => a -> a |
96 | | }}} |
97 | | |
98 | | The second example might be a bit surprising. Other options: |
99 | | * Allow syntactic permutations of the predicates (i.e., compare them as sets of predicates rather then lists of predicates) |
100 | | * Use entailment: |
101 | | {{{ |
102 | | (forall as. ps => s) === (forall bs. qs => t) |
103 | | iff |
104 | | 1) forall bs. exist as. (qs |- ps) /\ (s = t), and |
105 | | 2) forall as. exist bs. (ps |- qs) /\ (s = t) |
106 | | }}} |
107 | | |
108 | | PROPOSAL: Use syntactic equivalence modulo |
109 | | * alpha renamimng |
110 | | * order/repetition of predicates (i.e. compare predicates as sets) |
111 | | |
112 | | == Constructors == |
113 | | |
114 | | Constructor that have polymorphic components cannot appear in the |
115 | | program without values for their polymorphic fields. For example, |
116 | | consider the following declaration: |
117 | | {{{ |
118 | | data T a = C Int (forall b. b -> a) a |
119 | | }}} |
120 | | The constructor function 'C' should always be applied to at least |
121 | | two arguments because the second argument is the last polymorphic component |
122 | | of 'C'. Here are some examples of how we can use 'C': |
123 | | {{{ |
124 | | ex1 :: a -> T a |
125 | | ex1 a = C 2 (const a) -- ok. |
126 | | |
127 | | ex2 = C 2 -- not ok, needs another argument. |
128 | | }}} |
129 | | (This issue is related to the treatment of rank-2 types and the choice here should be consistent with that extension.) |
130 | | |
131 | | The restriction that functions with rank-2 types are applied to all their polymorphic arguments ensures that all expressions have ordinary (i.e., non rank-2) types, as in Haskell 98. |
132 | | |
133 | | Here is an example that illustrates some of the difficulties that arise if we allow partially applied constructors: |
134 | | {{{ |
135 | | data T = C1 Int (forall a. (Eq a, Show a) => a -> a) |
136 | | | C2 (forall a. (Show a, Eq a) => a -> a) |
137 | | |
138 | | h :: a -> a -> Int |
139 | | h _ _ = 1 |
140 | | |
141 | | test = h (C1 1) C2 |
142 | | }}} |
143 | | |
144 | | |
145 | | |
146 | | == Pattern matching == |
147 | | |
148 | | We do not allow nested patterns on fields that have polymorphic types. |
149 | | In other words, when we use a constructor with a polymorphic field |
150 | | as a pattern, we allow only variable and wild-card patterns in the |
151 | | positions corresponding to the polymorphic fields. |
152 | | |
153 | | Example: |
154 | | {{{ |
155 | | newtype PolyList = C (forall a. [a]) |
156 | | |
157 | | polyNull (C []) = True -- disallowed, nested pattern on a poly. field |
158 | | polyNull _ = False |
159 | | }}} |
160 | | This is the behavior of both Hugs and GHC at present. |