Overriding functions / default type class instance methods

[RicovanBuren]

In Haskell, functions defined in typeclasses can directly be overridden with a default implementation. It is not possible to directly convert those classes to record types in Agda, because you cannot define a function in the field clause and also directly give an implementation in the record. A way to get around this, is to define those functions outside of the record and when defining an instance of the record explicitly calling the default implementation when those functions are not overridden, as proposed by @flupe

It would be nice if agda2hs had a feature that allows such records to be compiled to a Haskell typeclass and specify which Agda functions/definitions to use for default implementations.

[jespercockx]

We're currently discussing this at the Agda meeting. We have three proposals for how we could model default implementations on the Agda side.

First variant: have default implementations as definitions in the record + maybe a proof that you used the default implementation:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Data.Maybe.Base

record Ord (A : Set) : Set where
  field
    _<_ : A → A → Bool
    _>_ : A → A → Bool

  default_<_ : A → A → Bool
  default x < y = y > x

  default_>_ : A → A → Bool
  default x > y = y < x

  field
    isDefault< : Maybe (_<_ ≡ default_<_)
    isDefault> : Maybe (_>_ ≡ default_>_)

open Ord {{...}}

OrdBool : Ord Bool
OrdBool .Ord._<_ false false = false
OrdBool .Ord._<_ false true  = true
OrdBool .Ord._<_ true  false = false
OrdBool .Ord._<_ true  true  = false
OrdBool .Ord._>_ = _
OrdBool .Ord.isDefault< = nothing
OrdBool .Ord.isDefault> = just refl

Problem: need to give the implementation of _>_ explicitly on the Agda side (the code above has unsolved constraints).

Second variant: have maybe an implementation for each field, and use the default implementation if it is nothing:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Data.Maybe
open import Data.Maybe.Relation.Unary.Any
open import Data.Sum
open import Data.Unit
open import Function

record Ord (A : Set) : Set where
  field
    _<'_ : Maybe (A → A → Bool)
    _>'_ : Maybe (A → A → Bool)

    minimalComplete : (Is-just _<'_) ⊎ (Is-just _>'_)

  _<_ : A → A → Bool
  _<_ = case minimalComplete of λ where
    (inj₁ p) → to-witness p
    (inj₂ p) → flip (to-witness p)

  _>_ : A → A → Bool
  _>_ = case minimalComplete of λ where
    (inj₁ p) → flip (to-witness p)
    (inj₂ p) → to-witness p

open Ord {{...}}

OrdBool : Ord Bool
OrdBool .Ord._<'_ = just (λ where
  false false → false
  false true → true
  true false → false
  true true → false)
OrdBool .Ord._>'_ = nothing
OrdBool .minimalComplete = inj₁ (just tt)

Problem: quite heavyweight, not easy to use on the Agda side.

Variant 3: have a separate record type for the default implementation:

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat as Nat using (Nat; zero; suc)

record Ord (A : Set) : Set where
  field
    _<_ : A → A → Bool
    _>_ : A → A → Bool

record OrdMinimal (A : Set) : Set where
  field
    _<_ : A → A → Bool

  ord : Ord A
  ord .Ord._<_ = _<_
  ord .Ord._>_ x y = y < x

open Ord {{...}}
open OrdMinimal using (ord)

OrdBool : Ord Bool
OrdBool = ord λ where
  .OrdMinimal._<_ false false → false
  .OrdMinimal._<_ false true  → true
  .OrdMinimal._<_ true  false → false
  .OrdMinimal._<_ true  true  → false

Problem: cannot have multiple minimal complete definitions.

[jespercockx]

After some more discussion and a nice idea by @UlfNorell to use an INLINE pragma we came to the following solution:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Data.Maybe.Base

open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

is-default : {A : Set} {x : A} → Maybe (x ≡ x)
is-default = just refl

try-default : Term → TC ⊤
try-default hole =
  catchTC (unify hole (def (quote is-default) []))
          (unify hole (con (quote nothing) []))

record Ord (A : Set) : Set where
  field
    _<_ : A → A → Bool
    _>_ : A → A → Bool

  default_<_ : A → A → Bool
  default x < y = y > x

  default_>_ : A → A → Bool
  default x > y = y < x

  field
    @(tactic try-default) isDefault< : Maybe (_<_ ≡ default_<_)
    @(tactic try-default) isDefault> : Maybe (_>_ ≡ default_>_)

  {-# INLINE default_<_ #-}
  {-# INLINE default_>_ #-}

open Ord {{...}}

instance
  OrdBool : Ord Bool
  OrdBool .Ord._<_ false false = false
  OrdBool .Ord._<_ false true  = true
  OrdBool .Ord._<_ true  false = false
  OrdBool .Ord._<_ true  true  = false
  OrdBool .Ord._>_ = default_>_

TODO: how to make sure we can actually recognize this type of definition and translate it to the proper Haskell code.

[omelkonian]

TODO: how to make sure we can actually recognize this type of definition and translate it to the proper Haskell code.

Seems to run fine without the INLINE pragma, is this necessary only for detecting stuff in the backend?

[jespercockx]

Weird, without the INLINE pragma the termination checker complains for me.

[omelkonian]

Weird, without the INLINE pragma the termination checker complains for me.

I am using Agda 2.6.1.3 btw.

[jespercockx]

Ah that explains it: on Agda 2.6.2 --auto-inline is no longer enabled by default, so you need to put the inline pragmas explicitly (or enable the flag).

[UlfNorell]

A few problems with the latest suggestion:

• The tactic might succeed with just refl for both methods. That actually happens in the given example since flip _>_ = flip (flip _<_) = _<_ definitionally. Could be fixed by a syntactic check in the macro.
• Termination checking for copattern definitions treat earlier projections as "smaller", so while the given definition of Ord Bool works, trying to define _<_ in terms of _>_ does not pass termination. This is a problem for classes like Show where you want to define either show or showsPrec, but very rarely both.

[omelkonian]

Latest iteration! Multiple minimal records, explicitly indicating the minimal sets:

{-# OPTIONS --no-auto-inline #-} -- needed in 2.6.1.3 downwards
module DefaultMethods where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.String renaming (primStringAppend to _++_)
open import Agda.Builtin.Char
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

-- open import Haskell.Prelude hiding (Show; showsPrec; )

infixr 9 _∘_
_∘_ : ∀ {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)
{-# INLINE _∘_ #-}

data Maybe {ℓ} (a : Set ℓ) : Set ℓ where
  Nothing : Maybe a
  Just    : a -> Maybe a

maybe : ∀ {ℓ₁ ℓ₂} {a : Set ℓ₁} {b : Set ℓ₂} → b → (a → b) → Maybe a → b
maybe n j Nothing  = n
maybe n j (Just x) = j x

ShowS : Set
ShowS = String → String

showString : String → ShowS
showString = _++_

showParen : Bool → ShowS → ShowS
showParen false s = s
showParen true  s = showString "(" ∘ s ∘ showString ")"

private variable a b : Set

foldl : (a → b → a) → a → List b → a
foldl c n []       = n
foldl c n (x ∷ xs) = foldl c (c n x) xs

defaultShowList : (a → ShowS) → List a → ShowS
defaultShowList _     []       = showString "[]"
defaultShowList shows (x ∷ xs) = showString "[" ∘ foldl (λ s x → s ∘ showString "," ∘ shows x) (shows x) xs ∘ showString "]"

record Show (a : Set) : Set where
  field
    show : a → String
    showPrec : Nat → a → ShowS
    showList : List a → ShowS

record Show₁ (a : Set) : Set where
  field
    showPrec : Nat → a → ShowS

  show : a → String
  show x = showPrec 0 x ""

  showList : List a → ShowS
  showList = defaultShowList (showPrec 0)

record Show₂ (a : Set) : Set where
  field
    show : a → String

  showPrec : Nat → a → ShowS
  showPrec _ x s = show x ++ s

  showList : List a → ShowS
  showList = defaultShowList (showPrec 0)

open Show ⦃ ... ⦄

{-# COMPILE AGDA2HS Show class Show₁ Show₂ #-}
-- NB: after looking up the minimal records, we can generate a GHC pragma {-# MINIMAL show | showPrec #-}
--    ++ overlapping definitions match (syntactically, after compiling Haskell!)
{- OUTPUT
class Show a where
  show :: a → String
  showPrec :: Int → a → ShowS
  showList :: List a → ShowS

  showPrec _ x s = show x ++ s
  show x = showPrec 0 x ""
  showList = defaultShowList (showPrec 0)
-}

SB : Show₂ Bool
SB .Show₂.show true  = "true"
SB .Show₂.show false = "false"

instance
  ShowBool : Show Bool
  ShowBool .show     = Show₂.show SB
  ShowBool .showPrec = Show₂.showPrec SB
  ShowBool .showList []       = showString ""
  ShowBool .showList (true ∷ bs) = showString "1" ∘ showList bs
  ShowBool .showList (false ∷ bs) = showString "0" ∘ showList bs

  ShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
  ShowMaybe {a = a} = record {Show₁ d}
    where
      d : Show₁ (Maybe a)
      d .Show₁.showPrec n Nothing = showString "nothing"
      d .Show₁.showPrec n (Just x) = showParen (9 < n) (showString "just " ∘ showPrec 10 x)

  ShowList : ⦃ Show a ⦄ → Show (List a)
  ShowList = record {Show₁ (λ where .Show₁.showPrec _ → showList)}

{-# COMPILE AGDA2HS ShowMaybe #-}
-- NB: assuming we always get copatterns (from outer-most records):
--    1. normal case (no minimality, just as before)
--    2. minimal primitive used (chase down definition and inline it)
--    3. minimal derived method used (ignore)

{- OUTPUT
instance Show Bool where
  show True = "true"
  show False = "false"

  showList [] = ....
  showList (true : ...
  showList (false : ...

instance Show a => Show (Maybe a) where
  showPrec n Nothing  = ...
  showPrec n (Just x) = ...

instance Show a => Show (List a) where
  showPrec _ = showList
-}

[jmchapman]

BTW: latest changes are in the 'defaults' branch I believe.

[omelkonian]

Before:

After:

Getting there :)

[omelkonian]

This is now supported, see merged PR #72.