[Haskell-cafe] Recursive constraints with type families
Li-yao Xia
lysxia at gmail.com
Sun Jan 23 21:05:13 UTC 2022
Hi Dmitriy,
On 2022-01-22 5:55 AM, Dmitriy Matrosov wrote:
>
> I see, thanks. But what i've tried to implement is type-level countdown:
>
[...]
>>
>> import GHC.TypeLits
>> import Data.Proxy
>> import Data.Kind
>> import qualified Fcf as F
>>
>> type C :: Nat -> Constraint
>> type family C x where
>> C 0 = KnownNat 0
>> C x = (KnownNat x, C (x - 1))
>>
>> countDown :: forall (n :: Nat). C n => Proxy n -> String
>> countDown _ = let x = natVal (Proxy @n)
>> in if x > 0
>> then show x ++ " " ++ countDown (Proxy @(n - 1))
>> else "end"
>
> This code does not compile
The condition (x > 0) does not propagate any information at the type
level. Such a thing is a feature of dependently typed languages, which
Haskell is not. The compiler does not know that n > 0 in the first
branch, so the constraint (C n) remains stuck.
> If i try to get rid of cases in type family:
>
>> type C2 :: Nat -> Constraint
>> type family C2 x where
>> C2 x = F.If (F.Eval (x F.> 0))
>> (KnownNat x, C2 (x - 1))
>> (KnownNat 0)
>
> ghc eats all memory and hangs during type family calculation:
>
> *Main> :k! C2 3
> ^CInterrupted.
> *Main>
[...]
> May be someone can explain me, why it hangs? I'll be very grateful.
The rule of thumb here is that if a type family can be unfolded, it will
be, regardless of context. Since there is only one clause, (C2 x) can
always be unfolded, and then C2 (x-1) will be unfolded (regardless of
whether the "If" condition is true or false) and then (C2 ((x-1)-1)), etc.
There is a trick with first-class-families to control evaluation with
the Eval type family, by making the branches reduce to uninterpreted
symbols, rather than type family applications.
Two key components of this trick:
- C2 must be a first-class type family (an "uninterpreted symbol")
- Eval must be applied outside of If
data C2 :: Nat -> F.Exp Constraint
type instance F.Eval (C2 x) =
(KnownNat x,
F.Eval (F.If (F.Eval (x F.> 0))
(C2 (x - 1))
(F.Pure (() :: Constraint))))
ghci:
> :k! F.Eval (C2 3)
F.Eval (C2 3) :: Constraint
= (KnownNat 3,
(KnownNat 2, (KnownNat 1, (KnownNat 0, () :: Constraint))))
> And the other question, is how then should i implement such type-level
> count
> down function?
To make constraints sensitive to control-flow, you need at least GADTs.
A general solution is provided by singletons, to simulate dependent
types in Haskell. For small tasks though, it's often easier to make your
own singletons.
One version of countdown looks like this:
countdown :: forall n. F.Eval (C2 n) => Proxy n -> String
countdown _ =
case getBool @(F.Eval (n F.> 0)) of
STrue -> show (natVal @n Proxy) ++ " " ++ countdown @(n-1) Proxy
SFalse -> "boom"
Where the comparison (n > 0) is done at the type level and reflected by
a boolean singleton value, of type SBool:
data SBool (a :: Bool) where
SFalse :: SBool 'False
STrue :: SBool 'True
Of course, the compiler doesn't know whether n is positive, so this
information must be provided as a constraint (or derived somehow):
-- Add IsBool constraint in C2, for every If condition
data C2 :: Nat -> F.Exp Constraint
type instance F.Eval (C2 x) =
(KnownNat x,
IsBool (F.Eval (x F.> 0)),
F.Eval (F.If (F.Eval (x F.> 0))
(C2 (x - 1))
(F.Pure (() :: Constraint))))
The IsBool class turns a known type-level boolean into a boolean
singleton value indexed by that same boolean:
class IsBool b where
getBool :: SBool b
instance IsBool 'True where
getBool = STrue
instance IsBool 'False where
getBool = SFalse
Full gist: https://gist.github.com/Lysxia/cf47807bbbcbb572896b350d66162a25
Regards,
Li-yao
More information about the Haskell-Cafe
mailing list