Created
September 23, 2022 23:41
-
-
Save zliu41/bfe4943400b665174e7071f3bd936770 to your computer and use it in GitHub Desktop.
Define Fix via HFix
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| module FixViaHFix where | |
| import Data.Functor.Identity | |
| import Data.Kind | |
| type HFix :: forall k. ((k -> Type) -> k -> Type) -> k -> Type | |
| newtype HFix f i = HFix {hunFix :: f (HFix f) i} | |
| type Hoist :: (Type -> Type) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Type | |
| newtype Hoist f w g = Hoist {unHoist :: g (f (w Identity))} | |
| type Fix :: (Type -> Type) -> Type | |
| type Fix f = HFix (Hoist f) Identity | |
| fix :: forall f. f (Fix f) -> Fix f | |
| fix = HFix . Hoist . Identity | |
| unfix :: forall f. Fix f -> f (Fix f) | |
| unfix = runIdentity . unHoist . hunFix |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment