Skip to content

Instantly share code, notes, and snippets.

@ekmett ekmett/Closed.hs
Created Oct 21, 2017

Embed
What would you like to do?
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
@sellout

This comment has been minimized.

Copy link

commented Oct 31, 2017

I see TypeApplications is enabled, but it looks like you don’t use the extension at all, and instead use Proxy. Did you start by using @ and then determine it didn’t work, or is Proxy less obscure, or am I just confused, or what?

@ekmett

This comment has been minimized.

Copy link
Owner Author

commented Nov 4, 2017

I did. I was going to write it TypeApplications style, then forgot. =)

@ekmett

This comment has been minimized.

Copy link
Owner Author

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

This comment has been minimized.

Copy link

commented Mar 30, 2018

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
You can’t perform that action at this time.