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

@sellout sellout 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

@ekmett ekmett 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

@ekmett 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

This comment has been minimized.

Copy link

@lukaszlew lukaszlew 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.