Skip to content

Instantly share code, notes, and snippets.

@as-capabl as-capabl/kequiv.hs
Created Jul 11, 2018

Embed
What would you like to do?
Path inductionで型レベル同値関係から値レベル同値関係を導く
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications, TypeInType, GADTs, RankNTypes #-}
import GHC.Types
import Data.Type.Equality
import Unsafe.Coerce
-- 仮定:Path Induction
indEquiv ::
forall k (t :: forall (x :: k) (y :: k). (x :~: y) -> Type).
(forall x. t ('Refl :: x :~: x)) -> forall a b (p :: a :~: b). t p
indEquiv f = unsafeCoerce f
-- ヘルパ
data SEq a b (p :: a :~: b)
where
SRefl :: SEq a a Refl
sRefl :: forall x. SEq x x ('Refl :: x :~: x)
sRefl = SRefl
-- 型レベル同値関係 → 値レベル同値関係
singEq :: forall x y (p :: x :~: y). x :~: y
singEq = case (indEquiv sRefl :: SEq x y p) of {SRefl -> Refl}
main :: IO ()
main = putStrLn $ castWith (singEq @ String @ String @ 'Refl) $ "Hello, world!"
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.