Created
April 23, 2016 07:36
-
-
Save func-hs/f8d59d4a94598d615fbb4b2626d8ff3c to your computer and use it in GitHub Desktop.
Listを依存型っぽくしてみようとしただけの何か
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-#LANGUAGE GADTs, KindSignatures, DataKinds, TypeOperators, TypeFamilies#-} | |
import GHC.TypeLits | |
data DList :: Nat -> * -> * where | |
DNil :: DList 0 a | |
DCons :: a -> DList n a -> DList (n + 1) a | |
append :: DList n a -> DList m a -> DList (n + m) a | |
append = undefined | |
main = return () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment