Closed kinds aren't as closed as you'd think
{-# language PolyKinds, DataKinds, RankNTypes, TypeApplications, ScopedTypeVariables, TypeFamilies, FlexibleInstances #-} | |
import Data.Proxy | |
class KnownUnit (k :: ()) where | |
reflect :: Proxy k -> Int | |
instance KnownUnit '() where | |
reflect _ = 0 | |
instance KnownUnit x => KnownUnit (f x) where | |
reflect _ = 1 + reflect (Proxy :: Proxy x) | |
type family Succ :: k -> k | |
reify :: Int -> (forall k. KnownUnit k => Proxy k -> r) -> r | |
reify 0 f = f (Proxy :: Proxy '()) | |
reify n f = reify (n - 1) $ \(Proxy :: Proxy k) -> f (Proxy :: Proxy (Succ k)) | |
-- ghci> reify 23 reflect | |
-- 23 |
This comment has been minimized.
This comment has been minimized.
I did. I was going to write it TypeApplications style, then forgot. =) |
This comment has been minimized.
This comment has been minimized.
I mentioned it in the tweet that originally linked here, but the technique that I used here is originally due to aarvar. |
This comment has been minimized.
This comment has been minimized.
Here's a reexposition of Edwad's example using type applications. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This comment has been minimized.
I see
TypeApplications
is enabled, but it looks like you don’t use the extension at all, and instead useProxy
. Did you start by using@
and then determine it didn’t work, or isProxy
less obscure, or am I just confused, or what?