Tail recursion and type level functions?

Learn
#1

The aoc 20 d22 problem (crabcombat) solution on the value level is such that if you make a little change and loose the tail recursion, the running time explodes from some seconds to one hour or something. E.g. using <> instead of ++ does that.

I wanted to see (and as a practice solution on type-level programming), how ghc and ghci handle it.

The actual solution is as short and neat as on value level (see https://github.com/gspia/fcf-containers/blob/master/examples/Crabcombat.hs for fully working example).

-- :kind! Eval (PlayGame '[] ExampleInput)
data PlayGame :: [([Nat],[Nat])] -> ([Nat],[Nat]) -> Exp ([Nat],Player)
type instance Eval (PlayGame _ '( p1 ': ps , '[])) = '( p1 ': ps, 'P1)
type instance Eval (PlayGame _ '( '[], p2 ': ps)) = '( p2 ': ps , 'P2)
type instance Eval (PlayGame hist '( v1 ': r1, v2 ': r2)) = Eval
    (If (Eval (Elem '(v1 ': r1, v2 ': r2) hist ))
        (Pure '( Eval (r1 ++ '[v1,v2]), 'P1)  )
        (If ( Eval (Eval (v1 <= Eval (Length r1)) && Eval (v2 <= Eval (Length r2)) ))
            (If (Eval ( TyEq (Eval (PlayGame '[] '( Eval (Take v1 r1), Eval (Take v2 r2)) ) ) 'P1))
                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(Eval (r1 ++ '[v1,v2]), r2))
                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(r1, Eval (r2 ++ '[v2,v1])))
            )
            (If (Eval (v1 > v2))
                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(Eval (r1 ++ '[v1,v2]), r2))
                (PlayGame ('( v1 ': r1, v2 ': r2) ': hist) '(r1, Eval (r2 ++ '[v2,v1])))
            )
        )
    )

When trying out with full problem input, the GHC refuses to compile it and ghci gets Killed.
(On my machine I think this worked with 14 Nat lists but not with 15 Nat lists.)

Are there other flags than -freduction-depth=0 that could be used here?

(With the small example problem input given at the aoc problem description, this works nicely.)

1 Like