I have a typeclass, which imposes a KnownNat constraint:

class KnownNat (Card a)=> HasFin a wheretype Card a :: Nat...

And, I have instances of this class for several basic "building block" types:

instance HasFin () wheretype Card ()=1...instance HasFin Bool wheretype Card Bool=2...

I plan to build many "composite" types out of these building block types, using sums and products. Currently, I'm having to explicitly write a composite KnownNat constraint, when I instance HasFin for one of these composite types:

instance (HasFin a, HasFin b, KnownNat (Card a + Card b))=> HasFin (Either a b) wheretype Card (Either a b)=Card a + Card b...

I would really like to not have to write: KnownNat (Card a + Card b), in the code above.

Is there any type checker plug-in, which is capable of automatically extrapolating from (HasFin a, HasFin b)=> to (KnownNat (Card a + Card b))=> ?

Failing that, can I write an entailment, which provides the same extrapolation?

share|improve this question

    Yes there is such a plugin! ghc-typelits-knownnat

    Example usage:

    -- Install ghc-typelits-knownnat via your favorite build tool like any other package-- then only this line needs to be added to enable the plugin{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-- Nothing special to be done otherwise, type-level programming as usual.{-# LANGUAGE DataKinds #-}{-# LANGUAGE FlexibleContexts #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}{-# LANGUAGE UndecidableInstances #-}module Card whereimport GHC.TypeLitsclass KnownNat (Card a)=> HasFin a wheretype Card a :: Natinstance HasFin () wheretype Card ()=1instance (HasFin a, HasFin b)=> HasFin (Either a b) wheretype Card (Either a b)=Card a + Card b

    Here's another technique without plugins, using the constraints library. It defines GADT to capture constraints and entailment as value-level dictionaries, and provides a few axioms, including the (KnownNat a, KnownNat b) :- KnownNat (a + b) entailment.

    {-# LANGUAGE AllowAmbiguousTypes #-}{-# LANGUAGE DataKinds #-}{-# LANGUAGE ScopedTypeVariables #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}{-# LANGUAGE UndecidableInstances #-}{-# LANGUAGE TypeApplications #-}module Card whereimport Data.Constraintimport Data.Constraint.Natimport GHC.TypeLitsclass HasFin a wheretype Card a :: Natcard :: Dict (KnownNat (Card a))instance HasFin () wheretype Card ()=1card=Dictinstance (HasFin a, HasFin b)=> HasFin (Either a b) wheretype Card (Either a b)=Card a + Card bcard=case (card @a, card @b, plusNat @(Card a) @(Card b)) of(Dict, Dict, Sub Dict) -> Dict
    share|improve this answer
    • Btw, do you have an example for this plugin usage? Like, some minimal project with steps to build and use? And explanation, if possible...– ShershFeb 13 at 19:00
    • I added some example code (and an alternative solution). There's not much to do, install the plugin like any other package, enable some command line options and that's it.– Li-yao XiaFeb 13 at 22:20

    Your Answer

     
    discard

    By posting your answer, you agree to the privacy policy and terms of service.

    Not the answer you're looking for? Browse other questions tagged or ask your own question.