Skip to content

Instantly share code, notes, and snippets.

@ekmett
Created October 21, 2017 09:50
Show Gist options
  • Save ekmett/ac881f3dba3f89ec03f8fdb1d8bf0a40 to your computer and use it in GitHub Desktop.
Save ekmett/ac881f3dba3f89ec03f8fdb1d8bf0a40 to your computer and use it in GitHub Desktop.
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
@ekmett
Copy link
Author

ekmett commented Nov 5, 2017

I mentioned it in the tweet that originally linked here, but the technique that I used here is originally due to aarvar.

@lukaszlew
Copy link

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