Не помню

Ага, типа f !@ Min

все равно мне мои решения больше нравятся, потому что они мои, но !@ это красиво конечно

foldOfVia конечно самый красивый имхо

-- <interactive>:1:1-17: error:
--     • Could not deduce (Equal Bool Int)
--         arising from a use of ‘defaultToInt’
--       from the context: Bool ~ Int

как же гхц вымораживает иногда

ну то есть какая-то предпосылка очевидно является ложной. И гхц не может из ложной предпосылки заключить, что Equal Bool Int выполняется

хотя очевидно, что из ложной предпосылки выполняется что угодно

Много хочешь)

это как предоставить Void, но не предоставить \case{} и какой-либо возможности его эмулировать

очень странно, ghc же должно быть все равно, ложная предпосылка или нет, именно для этого же коершины как полупервоклассные сущности и нужны

что такое Equal?

а стоп, ну да, много хочешь

выполняется-то что угодно, но нужно указать как это выполнить

разве в агде будет работать что-то вроде

x : (1 = 2) -> (10 = 20)
x refl = refl

?

пишешь x () и все

хм

удивительно

полный код (без прагм):

type Equal :: forall a b. a -> b -> Constraint
class Equal x y
instance Equal x x

type (~?~) :: forall a b. a -> b -> Constraint
class    (x ~~ y => Equal x y) => x ~?~ y
instance (x ~~ y => Equal x y) => x ~?~ y

-- >>> :t defaultToInt True
-- <interactive>:1:1-17: error:
--     • Could not deduce (Equal Bool Int)
--         arising from a use of ‘defaultToInt’
--       from the context: Bool ~ Int
--         bound by a quantified context at <interactive>:1:1
--     • In the expression: defaultToInt True
defaultToInt :: a ~?~ Int => a -> a
defaultToInt = id

а