Skip to content
This repository was archived by the owner on Apr 1, 2025. It is now read-only.

Commit 8355060

Browse files
committed
Define a fixpoint over rank-n quantified mendler-style recursive functions.
1 parent 89cdd3b commit 8355060

File tree

1 file changed

+9
-1
lines changed

1 file changed

+9
-1
lines changed

semantic-core/src/Analysis/Eval.hs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards #-}
1+
{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables #-}
22
module Analysis.Eval
33
( eval
44
, prog1
@@ -9,6 +9,7 @@ module Analysis.Eval
99
, prog6
1010
, ruby
1111
, Analysis(..)
12+
, fix
1213
) where
1314

1415
import Control.Effect.Fail
@@ -26,6 +27,13 @@ import Data.Text (Text)
2627
import GHC.Stack
2728
import Prelude hiding (fail)
2829

30+
fix :: forall f a b
31+
. ((forall x . (x -> a) -> f x -> b) -> (forall x . (x -> a) -> f x -> b))
32+
-> (forall x . (x -> a) -> f x -> b)
33+
fix f = x
34+
where x :: (x -> a) -> f x -> b
35+
x = f x
36+
2937
eval :: ( Carrier sig m
3038
, Member (Reader Loc) sig
3139
, MonadFail m

0 commit comments

Comments
 (0)