ograniczające ograniczenia

Question

mogę napisać następujący:

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

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

I wszystko jest dobrze. Przypuszczalnie GHC może uzyskać Integral z Num, więc wszystko jest w porządku.

mogę być nieco tricker, ale nadal jestem w porządku:

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 

Więc powiedzmy, że chcę uogólniać to tak:

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

Teraz oczywiście będzie pluć manekin, ponieważ GHC nie może wyprowadzić c2 z c1, ponieważ c2 nie jest ograniczony.

Co muszę dodać do podpisu typu g, aby powiedzieć, że "można uzyskać c2 z c1"?

Answer 1

Pakiet constraints zapewnia rozwiązanie tego problemu poprzez jego :- („pociąga za sobą”) typ:

{-# 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 

Następnie przepuszczając odpowiedni dowód, można odzyskać pierwotną przykład:

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

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

W rzeczywistości g jest jedynie odwrócone i wyspecjalizowaną wersję operatora \\:

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

g' = flip (\\) 

Jeśli masz czas, rozmowa Edwarda Kmetta "Type Classes vs the World" jest wspaniałym wprowadzeniem do tego, jak to wszystko działa.