Skip to content

Instantly share code, notes, and snippets.

@notogawa
Created Jun 22, 2018
Embed
What would you like to do?
{-# LANGUAGE GADTs #-}
module FooOrBar (someFun, Foo(..), Bar(..)) where
data Foo = Foo deriving Show
data Bar = Bar deriving Show
-- 「a が Foo か Bar である」という命題 (を explicit parameter として扱うため)の定義
data FooOrBarExplicitParameter a where
IsFoo :: FooOrBarExplicitParameter Foo -- 「a が Foo である」という証明オブジェクト
IsBar :: FooOrBarExplicitParameter Bar -- 「a が Bar である」という証明オブジェクト
-- explicit parameter を implicit 化 (してConstraintに置く)
-- 正攻法ではこのclassのinstanceをmodule外部で増やせないので閉じている
class FooOrBarImplicitParameter a where fooBar :: FooOrBarExplicitParameter a
instance FooOrBarImplicitParameter Foo where fooBar = IsFoo
instance FooOrBarImplicitParameter Bar where fooBar = IsBar
someFun :: (FooOrBarImplicitParameter a, Monad m) => m a
someFun = someFun' fooBar where -- implicit parameter になってる explicit parameter を引き出す
someFun' :: Monad m => FooOrBarExplicitParameter a -> m a -- explicit parameter でGADTのパターンマッチ(=「a が Foo か Bar である」という証明オブジェクトに対するdestruct操作)
someFun' IsFoo = return Foo -- 「a が Foo である」 (a ~ Foo のunificationが入った)ケースなので m Foo を与える
someFun' IsBar = return Bar -- 「a が Bar である」 (a ~ Bar のunificationが入った)ケースなので m Bar を与える
{- 実行例
> someFun :: IO Foo
Foo
> someFun :: IO Bar
Bar
> someFun :: IO Int
<interactive>:2:1: error:
• No instance for (FooOrBarImplicitParameter Int)
arising from a use of ‘someFun’
• In the expression: someFun :: IO Int
In an equation for ‘it’: it = someFun :: IO Int
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment