typeclasses: interface + instance vs data + @instance

[oxinabox]

I haven't managed to workout the difference between using interface and instance
and using data and @instance.

E.g. from the prelude:

data Integral a:Type =
  MkIntegral (a->a->a) (a->a->a) -- idiv, rem

@instance int64Integral : Integral Int64 = MkIntegral (\x:Int64 y:Int64. %idiv x y) (\x y. %irem x y)

vs also from the prelude:

interface Add a:Type where
  add : a -> a -> a
  sub : a -> a -> a
  zero : a

instance float64Add : Add Float64 where
  add = \x:Float64 y:Float64. %fadd x y
  sub = \x:Float64 y:Float64. %fsub x y
  zero = FToF64 0.0

The syntax is different but the purpose seems the same?

[apaszke]

data and @instance is really how interface and instance are implemented. The latter are a newer and nicer version of the API, and they should be preferred. But I wouldn't be surprised if some more advanced features (superclasses perhaps?) don't fully work with the newer API.

If you feel like it, we would gladly accept PRs that upgrade prelude to the new syntax!