Instantly share code, notes, and snippets.

Embed
What would you like to do?
A case for Dependent Types
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
-- Support for https://nunoalexandre.com/2018/01/28/a-case-for-dependent-types
data ValueType = StringType | IntType
data Value :: ValueType -> * where
StringValue :: String -> Value 'StringType
IntValue :: Int -> Value 'IntType
resetWithDefault :: Value a -> Value a
resetWithDefault (StringValue _) = StringValue "Hello, world!"
resetWithDefault (IntValue _) = IntValue 3
serious :: Value 'StringType -> Value 'StringType
serious (StringValue str) = StringValue $ str ++ "!"
foo :: Value 'StringType -> Value 'IntType
foo (StringValue _) = IntValue 3
bar :: Value a -> Value a
-- Compiling error as 'IntValue' does not match 'StringValue'
bar (StringValue str) = IntValue 3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment