matt-noonan/gdp

code:hs

newtype Named name a = Named a -- nameは幽霊型

type role Named nominal nominal

type a ~~ name = Named name a

name :: a -> (forall name. a ~~ name -> t) -> t

name x k = k (coerce x)

利用者に任意のnameを付けさせずに、nameを与えている

existなnameを指定している感じ

rank-2 typeを使わない場合、以下のような定義になる

code:hs

any_name :: a -> (a ~~ name)

any_name = coerce

しかし、これだと利用者が自在にnameを付けられるため、安全でなくなる

code:hs

class The d a | d -> a where

the :: d -> a

default the :: Coercible d a => d -> a

the = coerce

code:hs

instance The (a ~~ name) a

幽霊型とセットの値から、データを取り出す

code:hs

newtype SortedBy comp a = SortedBy a

instance The (SortedBy comp a) a

code:hs

data IsCons xs

data IsNil xs

data p == q

-- API functions

gdpHead xs = head (the xs)

gdpRev xs = defn (reverse (the xs))

length' xs = defn (length (the xs))

-- Names for API functions

newtype Length xs = Length Defn

newtype Reverse xs = Reverse Defn

-- Lemmas

rev_length :: Proof (Length (Reverse xs) == Length xs)

rev_length = axiom

rev_rev :: Proof (Reverse (Reverse xs) == xs)

rev_rev = axiom

rev_cons :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))

rev_cons _ = axiom

そのlemmaを型で定義する