On Sep 30, 2010, at 1:39 AM, Patrick Browne wrote:
I think my original question can be rephrased as:
Can type classes preserve satisfaction under the the expansion
sentences
(signature/theory morphisms inducing a model morphism).
According to [1] expansion requires further measures
Alexander Solla wrote:
Doing similar constructions with type classes is possible. I think you
might have to use witness types (or even a nice functorial wrapper
around your target value in the original algebra, or both) to do
generalizations of type classes. For example:
class Uneditable
On 09/28/2010 03:03 AM, Patrick Browne wrote:
I had a look at the types of a and a’.
*Main :t a
a :: forall a obj. (Uneditable obj) = a - obj
*Main :t a'
a' :: forall witness a obj. (Refactored obj witness) = Maybe (a - obj)
Could you explain the example a little more.
This is going to
Alexander Solla wrote:
On 09/26/2010 01:32 PM, Patrick Browne wrote:
Bigger how? Under logical implication and its computational analogue?
That is to say, do you want the model to be more SPECIFIC, describing a
smaller class of objects more richly (i.e, with more logical
implications to
On 09/27/2010 12:25 AM, Patrick Browne wrote:
Alexander Solla wrote:
On 09/26/2010 01:32 PM, Patrick Browne wrote:
/
Bigger how? Under logical implication and its computational analogue?
That is to say, do you want the model to be more SPECIFIC, describing a
smaller class of objects more
Hi,
Below is an assumption (which could be wrong) and two questions.
ASSUMPTION 1
Only smaller models can be specified using the sub-class mechanism.
For example if we directly make a subclass A = B then every instance of
B must also be an instance of A (B implies A or B is a subset of A).
Hence,
On 09/26/2010 01:32 PM, Patrick Browne wrote:
Hi,
Below is an assumption (which could be wrong) and two questions.
ASSUMPTION 1
Only smaller models can be specified using the sub-class mechanism.
For example if we directly make a subclass A = B then every instance of
B must also be an
