Skip to content

Instantly share code, notes, and snippets.

@bradparker bradparker/Ind.hs
Created Jul 28, 2019

Embed
What would you like to do?
Trying to figure out B. Milewski's slide from Lambda Jam 2019
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall #-}
module Ind where
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import GHC.TypeNats (Nat, KnownNat, type (+), type (-))
import GHC.TypeLits (natVal)
-- data Nat where
-- Z :: Nat
-- S :: Nat -> Nat
-- deriving instance Show Nat
data Vec (n :: Nat) (a :: Type) where
Nil :: Vec 0 a
Cons :: a -> Vec n a -> Vec (1 + n) a
deriving instance Show a => Show (Vec n a)
ind
:: forall (a :: Type) (n :: Nat)
. KnownNat n
=> Vec 0 a
-> ( forall (m :: Nat)
. KnownNat m
=> Proxy m
-> Vec m a
-> Vec (1 + m) a
)
-> Proxy n
-> Vec n a
ind base step nProxy =
if natVal nProxy == 0
then base -- Type error ... fair enough
else step (Proxy @(n - 1)) (ind base step (Proxy @(n - 1))) -- Type error
-- The second type error is pretty interesting to me.
--
-- It wants to know that `n ~ 1 + (n - 1)`.
-- If you add that to the context then it wants to know that `(n - 1) ~ (1 + (n - 1)) - 1` ...
-- And so on. Cool.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.