HList 정의에 대한 이해

Question

저는 하스켈에 비교적 새로 왔으며, HList의 정의 중 하나를 이해하려고합니다.

• 내가보고있어 '[] 및 (x ': xs) 구문은 무엇인가

  data instance HList '[] = HNil 
  newtype instance HList (x ': xs) = HCons1 (x, HList xs) 
  pattern HCons x xs = HCons1 (x, xs) 
  

  나는 몇 가지 구체적인 질문이 있습니까? 그것은 거의 그것이 variadic 타입 매개 변수에 패턴 매칭하는 것처럼 보이지만 전에는이 구문을 본 적이 없으며 Haskell의 variadic 타입 매개 변수에도 익숙하지 않습니다. 나는 이것이 GHC's Type Families의 일부라고 추측 하겠지만, 나는 링크 된 페이지에서 이것에 대해 아무 것도 보지 않으며 Google에서 구문을 검색하기가 다소 어렵다. HCons1의 권투를 피하는 이외의 튜플 (대신 두 개의 필드와 data 선언)와 newtype 선언을 사용하여 어떤 점

• 있습니까?

Answer 1

먼저 정의의 일부가 누락되었습니다 (data family 선언 자체).

data family HList (l :: [*]) 
data instance HList '[] = HNil 
newtype instance HList (x ': xs) = HCons1 (x, HList xs) 

이

가 호출합니다 ( TypeFamilies 확장에서 사용할 수)를 data family.

pattern HCons x xs = HCons1 (x, xs) 

이것은 양방향 패턴 (PatternSynonyms 확장명으로 사용 가능)입니다.

'[] 및 (x ': xs) 구문은 무엇입니까?

생성자 앞에 ' 마크가 표시되면 그 숫자는 promoted type-level counterparts입니다.통 사적 편의를.이 모든 DataKinds 확장을 통해 사용할 수 있습니다 promoted lists and tuples은 단지 여분의 틱이 필요합니다 (그리고 우리는 여전히 식 레벨 단점에 대한 빈 타입 수준의 목록과 ':에 대한 '[]를 작성 얻을.

을

?

예, 그것은 HList이 재현 role을 가지고 있는지 확인하는 것입니다 , HCons1의 권투를 피하는 이외의 튜플 (대신 두 개의 필드와 데이터 선언)와 newtype 선언을 사용하여 어느 시점이되는 너가 할 수있는 것을 의미한다. 사이의 간격은 HLists 사이이다. 이것은 단지 대답에 설명하기 위해 조금 너무 복잡하지만, 여기에 우리가 대신 newtype instance (없이 패턴)의

data instance HList (x ': xs) = HCons x (HList xs) 

이있을 때 우리가 원하는 일을하지 않는 경우의 예입니다. Int, Bool에 representationally 동일 다음 newtype의 고려, 각각 ()

newtype MyInt = MyInt Int 
newtype MyBool = MyBool Bool 
newtype MyUnit = MyUnit() 

우리가 포장 또는 자동으로 이러한 유형의 랩을 해제 할 coerce을 사용할 수 있습니다 리콜. 글쎄, 우리는 같은 일을 할 수 있기를 좋아하지만, 전체 HList에 대한 것 :

ghci> l = (HCons 3 (HCons True (HCons() HNil))) :: HList '[Int, Bool, ()] 
ghci> l' = coerce l        :: HList '[MyInt, MyBool, MyUnit] 

이것은 newtype instance 변형 작동하지만 때문에 역할을하지 data instance 하나. (즉 here에 대한 자세한.)

---

기술적

¹은, 전체적으로 data family에 대한 역할이 없다 : 역할이 각 instance/newtype 다를 수 있습니다 - 여기에 우리는 정말로에 HCons 경우 필요 그것이 표현력이 강해지는 표현이기 때문입니다. Check out this Trac ticket.

Answer 2

'[] 및 (x ': xs) 센스에서 입력 레벨 구문 목록하다는 것이 DataKinds language extension allows promoting types to kinds and constructors to types 단계; 즉 k이 어떤 종류 인 경우 '[k]도 종류이며 '[]은 종류가 '[k]이고 t :: k 및 ts :: '[k] 인 경우 t ': ts :: '[k] 인 경우입니다. 모든 것이 하나씩 이동합니다.

그래서 HList (x ': xs), x 및 xs 일치하는 두 종류의 : x 종류 * (예를 들어, Int)와 xs의 "정상적인"유형과 일치하는 종류 '[*] 다른 종류의 레벨 목록과 일치합니다. 오른쪽은 ( newtype) 데이터 유형이 이고, 매개 변수가 (x, HList xs) 인 생성자를 정의합니다. 나는 그것이로 표현 왜에 대한 두 번째 질문에 좋은 답변이없는

1 `HCons` True `HCons` HNil :: HList '[Int, Bool] 

:

예를 들어

, 우리는 패턴 동의어를 사용하여,

HCons1 (1, HCons1 (True, HNil)) :: HList '[Int, Bool] 

이 아니면 할 수 튜플을 포함한 newtype.