Last active
January 25, 2020 11:36
-
-
Save robrix/5a72dc9d171dc74a0449a6d14a7fd983 to your computer and use it in GitHub Desktop.
N is for Natural; zero, or more
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 DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeFamilyDependencies #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module NNat where | |
import GHC.TypeLits | |
-- Nat-indexed inductive naturals | |
data N (n :: Nat) where | |
Z :: N 0 | |
-- This is the important bit. | |
-- | |
-- We have to subtract on the left instead of adding on the right so that the type | |
-- family application (the - or +) does not offend the constraint solver when it | |
-- checks the kinds of the various N arguments to Plus'. The invisible kind params | |
-- passed to Plus' only complicate things further. | |
-- | |
-- Even with this, I had little success with a GADT providing witnesses of equality | |
-- between a non-indexed inductive N and Nat. This makes me suspect that I won’t be | |
-- able to use this to operate with Nat in my public types and only use N in the | |
-- internal implementations, or at least not directly. “Time will tell,” he said, | |
-- ominously. | |
S :: N (n - 1) -> N n | |
-- Addition of Nat-indexed naturals; any two arguments determine the third | |
-- Oleg did it first | |
class Plus (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b, b c -> a | |
instance (Plus' a b c, Plus' b a c) => Plus a b c | |
-- Addition of Nat-indexed naturals; the first argument and one other decide the last | |
class Plus' (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b | |
instance Plus' 'Z n n | |
instance Plus' m n o | |
=> Plus' ('S m) n ('S o) |
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 DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeFamilyDependencies #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module NNat where | |
import GHC.TypeLits | |
-- Nat-indexed inductive naturals | |
data N (n :: Nat) where | |
Z :: N 0 | |
-- As before, this is important for the definition of Plus'. | |
S :: N (n - 1) -> N n | |
-- /Injective/ mapping of Nat to N. | |
-- | |
-- This is where the type index of N really pays off: this type family can’t be made | |
-- injective without it, because the type variable is absent and the computation in | |
-- the subtraction is non-injective. So there’s no way for it to tell which n a non- | |
-- indexed 'S relates to. | |
type family FromNat (n :: Nat) = (n' :: N n) | n' -> n where | |
FromNat 0 = 'Z | |
FromNat n = 'S (FromNat (n - 1)) | |
-- This time around, let’s use Nat as the arguments to Plus, and map them to N in the | |
-- instance. | |
class Plus (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c, a c -> b, b c -> a | |
instance (Plus' (FromNat a) (FromNat b) (FromNat c), Plus' (FromNat b) (FromNat a) (FromNat c)) => Plus a b c | |
-- Addition of Nat-indexed naturals; the first argument and one other decide the last | |
class Plus' (a :: N na) (b :: N nb) (c :: N nc) | a b -> c, a c -> b | |
instance Plus' 'Z n n | |
instance Plus' m n o | |
=> Plus' ('S m) n ('S o) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment