| | 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. a -> 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) |
