Сдерживающие ограничения

Могу написать следующее:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}

f :: Integral a => (forall b. Num b => b) -> a
f = id

И все хорошо. Предположительно GHC может получить Integral из Num, так что все в порядке.

Я могу быть немного хитрее, но я все еще в порядке:

class Integral x => MyIntegral x
instance Integral x => MyIntegral x

class Num x => MyNum x
instance Num x => MyNum x

f' :: MyIntegral a => (forall b. MyNum b => b) -> a
f' = id

Итак, скажем, я хочу обобщить это, например:

g :: c2 a => (forall b. c1 b => b) -> a
g = id

Теперь очевидно, что это плюнет на пустышку, потому что GHC не может вывести c2 из c1, так как c2 не ограничено.

Что мне нужно добавить к сигнатуре типа g, чтобы сказать, что «вы можете получить c2 из c1»?


haskell ghc constraint-kinds
person Clinton    schedule 07.05.2017    source источник
comment
Когда вы говорите «вывести X из Y», я бы скорее сказал «вывести Y из X». В вашем первом примере мы имеем, что Integral t подразумевает Num t, а не наоборот. GHC должен извлечь Num словарь из переданного Integral словаря. И аналогично для других случаев, которые вы упомянули ниже.   -  person chi    schedule 07.05.2017

Ответы (1)


arrow_upward
7
arrow_downward

Пакет constraints предлагает решение этой проблемы с помощью типа :- ("entails"):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts

data Dict :: Constraint -> * where
    Dict :: a => Dict a

newtype a :- b = Sub (a => Dict b)
infixr 9 :-

g, g' :: c2 a => c2 a :- c1 a -> (forall b. c1 b => b) -> a
g (Sub Dict) x = x

Затем, передав соответствующий свидетель, мы можем восстановить исходный пример:

integralImpliesNum :: Integral a :- Num a
integralImpliesNum = Sub Dict

f :: Integral a => (forall b. Num b => b) -> a
f = g integralImpliesNum

На самом деле этот g является просто перевернутой и специализированной версией оператора \\:

(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
infixl 1 \\

g' = flip (\\)

Если у вас есть время, посмотрите доклад Эдварда Кметта "Классы типов против мира". отличное введение в то, как все это работает.

person Lambda Fairy    schedule 07.05.2017