문제
I tried to follow the program of the paper "Scrap your boilerpolate" Revolutions. Unfortunately, I found the program in the section lifted spine view does not compile in my GHC, could anybody point out where I am wrong?
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses,
FlexibleInstances, UndecidableInstances, ScopedTypeVariables,
NoMonomorphismRestriction, DeriveTraversable, DeriveFoldable,
DeriveFunctor, GADTs, KindSignatures, TypeOperators,
TemplateHaskell, BangPatterns
#-}
{-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-name-shadowing
-fwarn-monomorphism-restriction -fwarn-hi-shadowing
#-}
module LiftedSpine where
import Test.HUnit
-- Lifted Type View
newtype Id x = InID x
newtype Char' x = InChar' Char
newtype Int' x = InInt' Int
data List' a x = Nil' | Cons' (a x) (List' a x)
data Pair' a b x = InPair' (a x ) (b x)
data Tree' a x = Empty' | Node' (Tree' a x ) (a x) (Tree' a x)
data Type' :: ( * -> * ) -> * where
Id :: Type' Id
Char' :: Type' Char'
Int' :: Type' Int'
List' :: Type' a -> Type' (List' a)
Pair' :: Type' a -> Type' b -> Type' (Pair' a b)
Tree' :: Type' a -> Type' (Tree' a)
infixl 1 :->
data Typed' (f :: * -> *) a = (f a) :-> (Type' f)
size :: forall (f :: * -> *) (a :: *) . Typed' f a -> Int
size (Nil' :-> (List' a' )) = 0
size (Cons' x xs :-> List' a' ) =
size (xs :-> List' a') + size (x :-> a' )
해결책 2
we have to flip the two fields of (:->), i.e., the type has to be first and the annotated term has to be second. This is because pattern matching on GADTs and refinement is implicitly left-to-right in GHC.
다른 팁
The error I get when compiling this on GHC 6.12.1 is:
Couldn't match expected type `f' against inferred type `List' a'
`f' is a rigid type variable bound by
the type signature for `size' at /tmp/Foo.hs:34:15
In the pattern: Nil'
In the pattern: Nil' :-> (List' a')
In the definition of `size': size (Nil' :-> (List' a')) = 0
It seems like it fails to type check the pattern match of Nil'
because it hasn't realized that the right hand side pattern means that f
must be List'
. I suspect this may be because pattern matching is done left-to-right, because if I flip the order of the fields of Typed'
, so that List a'
gets matched before Nil'
, it compiles just fine.