structural equality가 적용될 때, 혹은 equality를 검사할 수 없을 때 - camelCase

nominal equality가 적용될 때 - PascalCase


structural : 구조를 쪼개서 재귀적으로 같은지 검사.

nominal : atomic한 값. 더 쪼갤 수 없으므로 이름으로 검사.

함수타입을 가지는 값들은 equality 검사가 불가능. 필요하다면 nominal한 래퍼타입을 만들어서 인자로 받아야함.


예시)

data Bool = True | False

data Nat = Z | S Nat

-- 타입/데이터 생성자는 더 쪼갤 수 없으니 nominal. 따라서 대문자로 시작.

-- open set인 경우(eq. Type) nominal이 강제됨.


nominal Eq

data Eq : Type -> Type

  MkEq : ((==) : a -> a -> Bool) ->

(forall x. x == x = True) ->

(forall x y. x == y = True -> y == x = True) ->

(forall x y z. x == y = True -> y == z = True -> x == z = True) ->

Eq a

-- 비교함수 (==)에 대한 래퍼타입.

-- Eq에 nominal 속성을 줬으므로 EqA :: Eq a를 (MkEq eq p q r = EqA)로 쪼개서 각각의 equality를 검사하는 대신, EqA 자체에 부여된 이름으로 검사.


EqNat : Eq Nat

EqNat = MkEq eq p q r where

eq = ..

p = ..

q = ..

r = ..

-- Eq Nat이 nominal하므로 EqNat은 대문자로 시작해야 함.