Well the other problems are more of a taste issue. With one instance per type we can leave the type system to infer the correct instance. this means that generic functions can have type signatures that take a single type parameter (or a minimal set of type parameters).
When we want a function that does some maths, uses some collections etc, then we might have: test :: Numeric s, Numeric t, Map t s, Map s t => s -> t We can then use test on something like: test 7 8.3 and the type-class dependencies are satisfied (or not) automatically. However if we use implicit parameters (or type parameters as in dependent types): test :: (Numeric s) -> (Numeric t) -> (Map t s) -> (Map s t) -> s -> t Now when we call we have to pass the right dictionaries: (test numeric_int numeric_float map_float_int map_int_float int float) Now it is up to the caller to ensure the dictionaries passed have the correct relationships to each other, so that the dictionary for the first argument related to the type of the second argument of the type associated with the third dictionary argument. I find this second way of structuring things gets really complicated very quickly, and has caused me problems in languages that require this sort of thing (ML, and Ada for example). Keean. On 2 January 2015 at 23:33, Geoffrey Irving <[email protected]> wrote: > On Fri, Jan 2, 2015 at 3:20 PM, Keean Schupke <[email protected]> wrote: > >> That is a compilation error, not unsoundness. Unless Iterator requires > >> Show, or the existential had an additional Show constraint, the call to > show > >> won't type check. > > > > I was wrong, it does require a type constraint like this: > > > > data Iterable = forall x . (Show (Value_Type x), Iterator x) => Iterable > x > > > > Further Haskell does not allow instances to declare arbitrary associated > > types like I thought, but instead you declare type-family like type-level > > functions inside the instance declaration, which is why you can declare > > "Show (Value_Type x)". > > > > However this does mean that it does not allow two instances of the same > type > > to declare different associated types, which is the problem I was > > describing. Haskell's associated types as not really associated types in > the > > sense of ML's associated types in modules. > > > > So my original point, expressed more precisely, that having multiple > > instances for a given type-class where the associated types differ is > > unsound, is not affected by this. > > I think we agree technically, in that I believe your point is that if > we assume that instances are coherent but have incoherent instances, > we get a contradiction. That's certain true, and the question is what > we lose by giving up that assumption. I'm right that we don't lose > decidability, and the syntax can stay exactly the same, what other > problems arise? > > Geoffrey > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
