6 people like it.

phantom types for dependent types; sized list; less than

Using phantom types to emulate simple dependent types and sized list. Inspired by: https://www.seas.upenn.edu/~sweirich/cis670/09/

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27: 
28: 
29: 
30: 
31: 
32: 
33: 
34: 
type Z = struct end
type S<'n> = struct end

type List<'n,'b> = L of 'b list
let empty : List<Z, 'b> = L []
let cons (b:'b) ((L bs) : List<'n, 'b>) : List<S<'n>,'b> = L (b::bs)
let head ((L bs):List<S<'n>,'b>) = List.head bs
let tail ((L bs):List<S<'n>,'b>) : List<'n,'b> = L(List.tail bs)

type LT<'n> = I of int
let z : LT<'n> = I 0
let s ((I x):LT<'n>) : LT<S<'n>> = I (x+1)

let rec lookup (i:LT<S<'n>>) (xs:List<S<'n>,'b>) : 'b =
    match i, xs with
    | I 0, L (x::_xs) -> x
    | I lt, L (x::xs) -> lookup (I (lt-1)) (L xs)

[<EntryPoint>]
let main args =
  let l3 : List<S<S<S<Z>>>,int> = cons 1 (cons 2 (cons 3 empty))
  let l2 = cons 0 (cons 1 (cons 2 (cons 3 empty)))
  
  let snd = lookup (s (s z)) l3
  
  printfn "%A; %A; %A" l3 l2 snd
  
  // Compiler error and ide warning
  // head empty
  // tail empty
  // lookup z empty
  // lookup (s z) empty
  // lookup (s(s(s z))) (cons 1 (cons 2 empty))
  0
type Z
type S<'n>
Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
    interface IReadOnlyList<'T>
    interface IReadOnlyCollection<'T>
    interface IEnumerable
    interface IEnumerable<'T>
    member GetReverseIndex : rank:int * offset:int -> int
    member GetSlice : startIndex:int option * endIndex:int option -> 'T list
    member Head : 'T
    member IsEmpty : bool
    member Item : index:int -> 'T with get
    member Length : int
    ...

--------------------
type List<'n,'b> = | L of 'b list
union case List.L: 'b list -> List<'n,'b>
type 'T list = List<'T>
val empty : List<Z,'b>
val cons : b:'b -> List<'n,'b> -> List<S<'n>,'b>
val b : 'b
val bs : 'b list
val head : List<S<'n>,'b> -> 'b
val head : list:'T list -> 'T
val tail : List<S<'n>,'b> -> List<'n,'b>
val tail : list:'T list -> 'T list
type LT<'n> = | I of int
union case LT.I: int -> LT<'n>
Multiple items
val int : value:'T -> int (requires member op_Explicit)

--------------------
type int = int32

--------------------
type int<'Measure> = int
val z : LT<'n>
val s : LT<'n> -> LT<S<'n>>
val x : int
val lookup : i:LT<S<'n>> -> xs:List<S<'n>,'b> -> 'b
val i : LT<S<'n>>
val xs : List<S<'n>,'b>
val x : 'b
val _xs : 'b list
val lt : int
val xs : 'b list
Multiple items
type EntryPointAttribute =
  inherit Attribute
  new : unit -> EntryPointAttribute

--------------------
new : unit -> EntryPointAttribute
val main : args:string [] -> int
val args : string []
val l3 : List<S<S<S<Z>>>,int>
val l2 : List<S<S<S<S<Z>>>>,int>
val snd : int
val printfn : format:Printf.TextWriterFormat<'T> -> 'T

More information

Link:http://fssnip.net/7YI
Posted:3 years ago
Author:Vankata
Tags: list , phantom types , #dependent types , playing with types , types